YES 18.524 H-Termination proof of /home/matraf/haskell/eval_FullyBlown_Fast/List.hs
H-Termination of the given Haskell-Program with start terms could successfully be proven:



HASKELL
  ↳ CR

mainModule List
  ((insert :: Float  ->  [Float ->  [Float]) :: Float  ->  [Float ->  [Float])

module List where
  import qualified Maybe
import qualified Prelude

  insert :: Ord a => a  ->  [a ->  [a]
insert e ls insertBy compare e ls

  insertBy :: (a  ->  a  ->  Ordering ->  a  ->  [a ->  [a]
insertBy x [] x : []
insertBy cmp x ys@(y : ys'
case cmp x y of
  GT-> y : insertBy cmp x ys'
  _-> x : ys


module Maybe where
  import qualified List
import qualified Prelude



Case Reductions:
The following Case expression
case cmp x y of
 GT → y : insertBy cmp x ys'
 _ → x : ys

is transformed to
insertBy0 y cmp x ys' ys GT = y : insertBy cmp x ys'
insertBy0 y cmp x ys' ys _ = x : ys



↳ HASKELL
  ↳ CR
HASKELL
      ↳ BR

mainModule List
  ((insert :: Float  ->  [Float ->  [Float]) :: Float  ->  [Float ->  [Float])

module List where
  import qualified Maybe
import qualified Prelude

  insert :: Ord a => a  ->  [a ->  [a]
insert e ls insertBy compare e ls

  insertBy :: (a  ->  a  ->  Ordering ->  a  ->  [a ->  [a]
insertBy x [] x : []
insertBy cmp x ys@(y : ys'insertBy0 y cmp x ys' ys (cmp x y)

  
insertBy0 y cmp x ys' ys GT y : insertBy cmp x ys'
insertBy0 y cmp x ys' ys _ x : ys


module Maybe where
  import qualified List
import qualified Prelude



Replaced joker patterns by fresh variables and removed binding patterns.
Binding Reductions:
The bind variable of the following binding Pattern
ys@(vy : vz)

is replaced by the following term
vy : vz



↳ HASKELL
  ↳ CR
    ↳ HASKELL
      ↳ BR
HASKELL
          ↳ COR

mainModule List
  ((insert :: Float  ->  [Float ->  [Float]) :: Float  ->  [Float ->  [Float])

module List where
  import qualified Maybe
import qualified Prelude

  insert :: Ord a => a  ->  [a ->  [a]
insert e ls insertBy compare e ls

  insertBy :: (a  ->  a  ->  Ordering ->  a  ->  [a ->  [a]
insertBy vx x [] x : []
insertBy cmp x (vy : vzinsertBy0 vy cmp x vz (vy : vz) (cmp x vy)

  
insertBy0 y cmp x ys' ys GT y : insertBy cmp x ys'
insertBy0 y cmp x ys' ys vw x : ys


module Maybe where
  import qualified List
import qualified Prelude



Cond Reductions:
The following Function with conditions
undefined 
 | False
 = undefined

is transformed to
undefined  = undefined1

undefined0 True = undefined

undefined1  = undefined0 False



↳ HASKELL
  ↳ CR
    ↳ HASKELL
      ↳ BR
        ↳ HASKELL
          ↳ COR
HASKELL
              ↳ Narrow

mainModule List
  (insert :: Float  ->  [Float ->  [Float])

module List where
  import qualified Maybe
import qualified Prelude

  insert :: Ord a => a  ->  [a ->  [a]
insert e ls insertBy compare e ls

  insertBy :: (a  ->  a  ->  Ordering ->  a  ->  [a ->  [a]
insertBy vx x [] x : []
insertBy cmp x (vy : vzinsertBy0 vy cmp x vz (vy : vz) (cmp x vy)

  
insertBy0 y cmp x ys' ys GT y : insertBy cmp x ys'
insertBy0 y cmp x ys' ys vw x : ys


module Maybe where
  import qualified List
import qualified Prelude



Haskell To QDPs


↳ HASKELL
  ↳ CR
    ↳ HASKELL
      ↳ BR
        ↳ HASKELL
          ↳ COR
            ↳ HASKELL
              ↳ Narrow
                ↳ AND
QDP
                    ↳ QDPSizeChangeProof
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primCmpNat(Succ(ww41500), Succ(ww41900)) → new_primCmpNat(ww41500, ww41900)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ CR
    ↳ HASKELL
      ↳ BR
        ↳ HASKELL
          ↳ COR
            ↳ HASKELL
              ↳ Narrow
                ↳ AND
                  ↳ QDP
QDP
                    ↳ QDPSizeChangeProof
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primPlusNat(Succ(ww5500), Succ(ww400000)) → new_primPlusNat(ww5500, ww400000)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ CR
    ↳ HASKELL
      ↳ BR
        ↳ HASKELL
          ↳ COR
            ↳ HASKELL
              ↳ Narrow
                ↳ AND
                  ↳ QDP
                  ↳ QDP
QDP
                    ↳ QDPSizeChangeProof
                  ↳ QDP
                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primMulNat(Succ(ww51000), Succ(ww363000)) → new_primMulNat(ww51000, Succ(ww363000))

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ CR
    ↳ HASKELL
      ↳ BR
        ↳ HASKELL
          ↳ COR
            ↳ HASKELL
              ↳ Narrow
                ↳ AND
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
QDP
                    ↳ QDPSizeChangeProof
                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primMulNat0(Succ(ww30000), ww40000) → new_primMulNat0(ww30000, ww40000)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ CR
    ↳ HASKELL
      ↳ BR
        ↳ HASKELL
          ↳ COR
            ↳ HASKELL
              ↳ Narrow
                ↳ AND
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
QDP
                    ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

new_insertBy01(Float(Pos(Zero), Neg(Succ(ww40100))), Float(Pos(Succ(ww3000)), Pos(Succ(Succ(Zero)))), ww41) → new_insertBy08(ww40100, ww3000, ww41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(ww40100)), Succ(ww40100)))
new_insertBy012(ww40000, ww40100, ww41, Succ(ww1020)) → new_insertBy058(Float(Pos(Succ(ww40000)), Neg(Succ(ww40100))), ww41)
new_insertBy7(:(ww410, ww411)) → new_insertBy01(ww410, Float(Neg(Zero), Neg(Succ(Zero))), ww411)
new_insertBy032(ww38, Pos(Succ(ww3900)), ww40, Neg(Succ(ww4100)), ww42, Zero) → new_insertBy070(ww38, ww3900, ww40, ww4100, ww42, new_primPlusNat0(new_primMulNat1(ww4100, ww3900), Succ(ww3900)))
new_insertBy10(:(ww410, ww411)) → new_insertBy01(ww410, Float(Pos(Zero), Neg(Succ(Succ(Zero)))), ww411)
new_insertBy0(ww19, Neg(Succ(ww2000)), ww21, Neg(Zero), ww23, Succ(ww560)) → new_insertBy1(ww21, Zero, ww23)
new_insertBy02(ww19, ww2000, ww21, ww2200, ww23, Succ(ww5600), Succ(Zero)) → new_insertBy088(ww19, ww2000, ww21, ww2200, ww23)
new_insertBy01(Float(Neg(Succ(ww40000)), Pos(Succ(ww40100))), Float(Neg(Zero), Neg(Succ(Zero))), :(ww410, ww411)) → new_insertBy01(ww410, Float(Neg(Zero), Neg(Succ(Zero))), ww411)
new_insertBy01(Float(Pos(Succ(ww40000)), Neg(Succ(ww40100))), Float(Neg(Zero), Pos(Succ(Succ(Zero)))), ww41) → new_insertBy038(ww40000, ww40100, ww41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(ww40100)), Succ(ww40100)))
new_insertBy079(ww44, ww4500, ww46, ww4700, ww48, Succ(ww32000), Zero) → new_insertBy080(ww44, ww4500, ww46, ww4700, ww48)
new_insertBy086(ww19, ww200, ww21, ww220, :(ww230, ww231)) → new_insertBy01(ww230, Float(Pos(Succ(ww21)), Neg(ww220)), ww231)
new_insertBy01(Float(Neg(Zero), Pos(Succ(ww40100))), Float(Neg(Succ(ww3000)), Neg(Succ(Succ(Zero)))), ww41) → new_insertBy049(ww40100, ww3000, ww41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(ww40100)), Succ(ww40100)))
new_insertBy01(Float(Pos(Zero), Neg(Succ(ww40100))), Float(Neg(Zero), Pos(Succ(Succ(Zero)))), ww41) → new_insertBy042(ww40100, ww41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(ww40100)), Succ(ww40100)))
new_insertBy017(ww40100, ww310000, ww41, Succ(ww1280)) → new_insertBy9(ww310000, ww41)
new_insertBy3(:(ww410, ww411)) → new_insertBy01(ww410, Float(Pos(Zero), Neg(Succ(Zero))), ww411)
new_insertBy085(ww19, ww200, ww21, ww220, :(ww230, ww231)) → new_insertBy01(ww230, Float(Pos(Succ(ww21)), Pos(ww220)), ww231)
new_insertBy01(Float(Neg(Zero), Neg(Succ(ww40100))), Float(Neg(Succ(ww3000)), Pos(Succ(Zero))), ww41) → new_insertBy4(ww3000, Succ(Zero), ww41)
new_insertBy019(ww25, Neg(Succ(ww2600)), ww27, Pos(Succ(ww2800)), ww29, Zero) → new_insertBy061(ww25, ww2600, ww27, ww2800, ww29, new_primPlusNat0(new_primMulNat1(ww2800, ww2600), Succ(ww2600)))
new_insertBy010(ww40100, ww3000, ww41, Succ(ww720)) → new_insertBy1(ww3000, Succ(Succ(Zero)), ww41)
new_insertBy045(ww44, Neg(Zero), ww46, Neg(Zero), ww48, Succ(ww3200)) → new_insertBy5(ww46, Zero, ww48)
new_insertBy01(Float(Pos(Zero), Pos(Succ(ww40100))), Float(Neg(Succ(ww3000)), Neg(Succ(Zero))), ww41) → new_insertBy5(ww3000, Succ(Zero), ww41)
new_insertBy087(ww19, ww2000, ww21, ww2200, ww23, Succ(ww5600), Succ(ww9000)) → new_insertBy087(ww19, ww2000, ww21, ww2200, ww23, ww5600, ww9000)
new_insertBy014(ww40000, ww40100, :(ww410, ww411), Succ(ww1080)) → new_insertBy01(ww410, Float(Pos(Zero), Neg(Succ(Succ(Zero)))), ww411)
new_insertBy022(ww40100, ww3000, ww310000, ww41, Succ(ww1590)) → new_insertBy1(ww3000, Succ(Succ(Succ(ww310000))), ww41)
new_insertBy083(ww44, ww4500, ww46, ww4700, ww48, Succ(ww32000), Zero) → new_insertBy084(ww44, ww4500, ww46, ww4700, ww48)
new_insertBy032(ww38, Neg(Succ(ww3900)), ww40, Pos(Succ(ww4100)), ww42, Zero) → new_insertBy069(ww38, ww3900, ww40, ww4100, ww42, new_primPlusNat0(new_primMulNat1(ww4100, ww3900), Succ(ww3900)))
new_insertBy0(ww19, Neg(Succ(ww2000)), ww21, Neg(Succ(ww2200)), ww23, Succ(ww560)) → new_insertBy02(ww19, ww2000, ww21, ww2200, ww23, ww560, new_primPlusNat0(new_primMulNat1(ww2200, ww2000), Succ(ww2000)))
new_insertBy01(Float(Neg(Succ(ww40000)), Neg(Succ(ww40100))), Float(Pos(Zero), Pos(Succ(Succ(Zero)))), ww41) → new_insertBy025(ww40000, ww40100, ww41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(ww40100)), Succ(ww40100)))
new_insertBy079(ww44, ww4500, ww46, ww4700, ww48, Succ(ww32000), Succ(ww35900)) → new_insertBy079(ww44, ww4500, ww46, ww4700, ww48, ww32000, ww35900)
new_insertBy01(Float(Pos(Zero), Pos(Succ(ww40100))), Float(Neg(Succ(ww3000)), Neg(Succ(Succ(Zero)))), ww41) → new_insertBy036(ww40100, ww3000, ww41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(ww40100)), Succ(ww40100)))
new_insertBy13(ww310000, :(ww410, ww411)) → new_insertBy01(ww410, Float(Neg(Zero), Neg(Succ(Succ(Succ(ww310000))))), ww411)
new_insertBy062(ww25, ww2600, ww27, ww2800, ww29, Succ(ww1750)) → new_insertBy1(ww27, Succ(ww2800), ww29)
new_insertBy01(Float(Pos(Zero), Neg(Succ(ww40100))), Float(Pos(Zero), Pos(Succ(Succ(Succ(ww310000))))), ww41) → new_insertBy015(ww40100, ww310000, ww41, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat1(ww310000, ww40100), Succ(ww40100)), Succ(ww40100)), Succ(ww40100)))
new_insertBy00(ww19, ww2000, ww21, ww2200, ww23, Succ(ww5600), Succ(Zero)) → new_insertBy06(ww19, ww2000, ww21, ww2200, ww23)
new_insertBy015(ww40100, ww310000, ww41, Succ(ww1220)) → new_insertBy8(ww310000, ww41)
new_insertBy01(Float(Pos(Succ(ww40000)), Neg(Succ(ww40100))), Float(Pos(Zero), Pos(Succ(Succ(Succ(ww310000))))), ww41) → new_insertBy011(ww40000, ww40100, ww310000, ww41, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat1(ww310000, ww40100), Succ(ww40100)), Succ(ww40100)), Succ(ww40100)))
new_insertBy00(ww19, ww2000, ww21, ww2200, ww23, ww560, Zero) → new_insertBy(ww21, Succ(ww2200), ww23)
new_insertBy0(ww19, Pos(Zero), ww21, Pos(Zero), ww23, Succ(ww560)) → new_insertBy(ww21, Zero, ww23)
new_insertBy019(ww25, Neg(Succ(ww2600)), ww27, Pos(Succ(ww2800)), ww29, Succ(ww1400)) → new_insertBy059(ww25, ww2600, ww27, ww2800, ww29, new_primPlusNat0(new_primMulNat1(ww2800, ww2600), Succ(ww2600)), ww1400)
new_insertBy045(ww44, Pos(Succ(ww4500)), ww46, Pos(Zero), ww48, Succ(ww3200)) → new_insertBy4(ww46, Zero, ww48)
new_insertBy036(ww40100, ww3000, ww41, Succ(ww2520)) → new_insertBy5(ww3000, Succ(Succ(Zero)), ww41)
new_insertBy056(ww40100, ww310000, ww41, Succ(ww4000)) → new_insertBy13(ww310000, ww41)
new_insertBy01(Float(Pos(Zero), Pos(Succ(ww40100))), Float(Neg(Zero), Neg(Succ(Succ(Succ(ww310000))))), ww41) → new_insertBy043(ww40100, ww310000, ww41, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat1(ww310000, ww40100), Succ(ww40100)), Succ(ww40100)), Succ(ww40100)))
new_insertBy018(ww40100, ww41, Succ(ww1320)) → new_insertBy10(ww41)
new_insertBy01(Float(Pos(Succ(ww40000)), Pos(Succ(ww40100))), Float(Neg(Zero), Neg(Succ(Succ(Zero)))), ww41) → new_insertBy040(ww40000, ww40100, ww41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(ww40100)), Succ(ww40100)))
new_insertBy01(Float(Neg(Succ(ww40000)), Pos(Succ(ww40100))), Float(Pos(Zero), Neg(Succ(Succ(Zero)))), ww41) → new_insertBy027(ww40000, ww40100, ww41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(ww40100)), Succ(ww40100)))
new_insertBy088(ww19, ww2000, ww21, ww2200, ww23) → new_insertBy1(ww21, Succ(ww2200), ww23)
new_insertBy087(ww19, ww2000, ww21, ww2200, ww23, Succ(ww5600), Zero) → new_insertBy088(ww19, ww2000, ww21, ww2200, ww23)
new_insertBy0(ww19, Pos(ww200), ww21, Neg(ww220), :(ww230, ww231), Succ(ww560)) → new_insertBy01(ww230, Float(Pos(Succ(ww21)), Neg(ww220)), ww231)
new_insertBy8(ww310000, :(ww410, ww411)) → new_insertBy01(ww410, Float(Pos(Zero), Pos(Succ(Succ(Succ(ww310000))))), ww411)
new_insertBy01(Float(Neg(Succ(ww40000)), Pos(Succ(ww40100))), Float(Neg(Zero), Neg(Succ(Succ(Zero)))), ww41) → new_insertBy053(ww40000, ww40100, ww41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(ww40100)), Succ(ww40100)))
new_insertBy01(Float(Neg(Zero), Neg(Succ(ww40100))), Float(Pos(Succ(ww3000)), Pos(Succ(Succ(Succ(ww310000))))), ww41) → new_insertBy020(ww40100, ww3000, ww310000, ww41, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat1(ww310000, ww40100), Succ(ww40100)), Succ(ww40100)), Succ(ww40100)))
new_insertBy01(Float(Pos(Zero), Pos(Succ(ww40100))), Float(Pos(Succ(ww3000)), Neg(Succ(Succ(Zero)))), ww41) → new_insertBy010(ww40100, ww3000, ww41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(ww40100)), Succ(ww40100)))
new_insertBy01(Float(Pos(Zero), Pos(Succ(ww40100))), Float(Pos(Zero), Neg(Succ(Succ(Succ(ww310000))))), ww41) → new_insertBy017(ww40100, ww310000, ww41, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat1(ww310000, ww40100), Succ(ww40100)), Succ(ww40100)), Succ(ww40100)))
new_insertBy01(Float(Pos(Succ(ww40000)), Neg(Succ(ww40100))), Float(Neg(Zero), Pos(Succ(Succ(Succ(ww310000))))), ww41) → new_insertBy037(ww40000, ww40100, ww310000, ww41, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat1(ww310000, ww40100), Succ(ww40100)), Succ(ww40100)), Succ(ww40100)))
new_insertBy026(ww40000, ww40100, ww310000, ww41, Succ(ww1950)) → new_insertBy9(ww310000, ww41)
new_insertBy045(ww44, Pos(Succ(ww4500)), ww46, Neg(Succ(ww4700)), ww48, Zero) → new_insertBy078(ww44, ww4500, ww46, ww4700, ww48, new_primPlusNat0(new_primMulNat1(ww4700, ww4500), Succ(ww4500)))
new_insertBy039(ww40000, ww40100, ww310000, ww41, Succ(ww2840)) → new_insertBy13(ww310000, ww41)
new_insertBy059(ww25, ww2600, ww27, ww2800, ww29, Succ(Succ(ww17900)), Succ(ww14000)) → new_insertBy063(ww25, ww2600, ww27, ww2800, ww29, ww17900, ww14000)
new_insertBy01(Float(Neg(Zero), Neg(Succ(ww40100))), Float(Pos(Succ(ww3000)), Pos(Succ(Succ(Zero)))), ww41) → new_insertBy021(ww40100, ww3000, ww41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(ww40100)), Succ(ww40100)))
new_insertBy0(ww19, Pos(Succ(ww2000)), ww21, Neg(Succ(ww2200)), ww23, Zero) → new_insertBy04(ww19, ww2000, ww21, ww2200, ww23, new_primPlusNat0(new_primMulNat1(ww2200, ww2000), Succ(ww2000)))
new_insertBy05(ww19, ww2000, ww21, ww2200, ww23, Succ(ww5600), Succ(ww8800)) → new_insertBy05(ww19, ww2000, ww21, ww2200, ww23, ww5600, ww8800)
new_insertBy027(ww40000, ww40100, ww41, Succ(ww1990)) → new_insertBy10(ww41)
new_insertBy045(ww44, Pos(Zero), ww46, Pos(Zero), ww48, Succ(ww3200)) → new_insertBy4(ww46, Zero, ww48)
new_insertBy01(Float(Neg(Succ(ww40000)), Neg(Succ(ww40100))), Float(Pos(Zero), Pos(Succ(Succ(Succ(ww310000))))), ww41) → new_insertBy024(ww40000, ww40100, ww310000, ww41, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat1(ww310000, ww40100), Succ(ww40100)), Succ(ww40100)), Succ(ww40100)))
new_insertBy01(Float(Pos(Zero), Neg(Succ(ww40100))), Float(Neg(Zero), Pos(Succ(Zero))), ww41) → new_insertBy6(ww41)
new_insertBy076(ww44, ww4500, ww46, ww4700, ww48, Succ(ww32000), Succ(Zero)) → new_insertBy084(ww44, ww4500, ww46, ww4700, ww48)
new_insertBy01(Float(Neg(Zero), Pos(Succ(ww40100))), Float(Neg(Zero), Neg(Succ(Succ(Succ(ww310000))))), ww41) → new_insertBy056(ww40100, ww310000, ww41, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat1(ww310000, ww40100), Succ(ww40100)), Succ(ww40100)), Succ(ww40100)))
new_insertBy076(ww44, ww4500, ww46, ww4700, ww48, ww3200, Zero) → new_insertBy5(ww46, Succ(ww4700), ww48)
new_insertBy045(ww44, Neg(Succ(ww4500)), ww46, Neg(Succ(ww4700)), ww48, Succ(ww3200)) → new_insertBy076(ww44, ww4500, ww46, ww4700, ww48, ww3200, new_primPlusNat0(new_primMulNat1(ww4700, ww4500), Succ(ww4500)))
new_insertBy024(ww40000, ww40100, ww310000, ww41, Succ(ww1890)) → new_insertBy8(ww310000, ww41)
new_insertBy2(:(ww410, ww411)) → new_insertBy01(ww410, Float(Pos(Zero), Pos(Succ(Zero))), ww411)
new_insertBy0(ww19, Pos(Succ(ww2000)), ww21, Pos(Zero), ww23, Succ(ww560)) → new_insertBy(ww21, Zero, ww23)
new_insertBy051(ww40000, ww40100, :(ww410, ww411), Succ(ww3740)) → new_insertBy01(ww410, Float(Neg(Zero), Pos(Succ(Succ(Zero)))), ww411)
new_insertBy045(ww44, Neg(Succ(ww4500)), ww46, Neg(Zero), ww48, Succ(ww3200)) → new_insertBy5(ww46, Zero, ww48)
new_insertBy075(ww44, ww4500, ww46, ww4700, ww48, Succ(ww32000), Succ(Zero)) → new_insertBy080(ww44, ww4500, ww46, ww4700, ww48)
new_insertBy01(Float(Pos(Zero), Pos(Succ(ww40100))), Float(Pos(Zero), Neg(Succ(Succ(Zero)))), ww41) → new_insertBy018(ww40100, ww41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(ww40100)), Succ(ww40100)))
new_insertBy4(ww46, ww470, :(ww480, ww481)) → new_insertBy01(ww480, Float(Neg(Succ(ww46)), Pos(ww470)), ww481)
new_insertBy070(ww38, ww3900, ww40, ww4100, ww42, Succ(ww2640)) → new_insertBy5(ww40, Succ(ww4100), ww42)
new_insertBy045(ww44, Neg(Zero), ww46, Neg(Succ(ww4700)), ww48, Succ(ww3200)) → new_insertBy5(ww46, Succ(ww4700), ww48)
new_insertBy06(ww19, ww2000, ww21, ww2200, ww23) → new_insertBy(ww21, Succ(ww2200), ww23)
new_insertBy044(ww40100, ww41, Succ(ww3120)) → new_insertBy14(ww41)
new_insertBy08(ww40100, ww3000, ww41, Succ(ww660)) → new_insertBy(ww3000, Succ(Succ(Zero)), ww41)
new_insertBy01(Float(Pos(Zero), Pos(Succ(ww40100))), Float(Pos(Zero), Neg(Succ(Zero))), ww41) → new_insertBy3(ww41)
new_insertBy037(ww40000, ww40100, ww310000, ww41, Succ(ww2780)) → new_insertBy11(ww310000, ww41)
new_insertBy034(ww40100, ww3000, ww41, Succ(ww2460)) → new_insertBy4(ww3000, Succ(Succ(Zero)), ww41)
new_insertBy01(Float(Neg(Zero), Neg(Succ(ww40100))), Float(Neg(Succ(ww3000)), Pos(Succ(Succ(Succ(ww310000))))), ww41) → new_insertBy046(ww40100, ww3000, ww310000, ww41, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat1(ww310000, ww40100), Succ(ww40100)), Succ(ww40100)), Succ(ww40100)))
new_insertBy083(ww44, ww4500, ww46, ww4700, ww48, Succ(ww32000), Succ(ww36100)) → new_insertBy083(ww44, ww4500, ww46, ww4700, ww48, ww32000, ww36100)
new_insertBy01(Float(Pos(Zero), Pos(Succ(ww40100))), Float(Neg(Succ(ww3000)), Neg(Succ(Succ(Succ(ww310000))))), ww41) → new_insertBy035(ww40100, ww3000, ww310000, ww41, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat1(ww310000, ww40100), Succ(ww40100)), Succ(ww40100)), Succ(ww40100)))
new_insertBy052(ww40000, ww40100, ww310000, :(ww410, ww411), Succ(ww3760)) → new_insertBy01(ww410, Float(Neg(Zero), Neg(Succ(Succ(Succ(ww310000))))), ww411)
new_insertBy01(Float(Neg(Zero), Pos(Succ(ww40100))), Float(Pos(Succ(ww3000)), Neg(Succ(Succ(Succ(ww310000))))), ww41) → new_insertBy022(ww40100, ww3000, ww310000, ww41, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat1(ww310000, ww40100), Succ(ww40100)), Succ(ww40100)), Succ(ww40100)))
new_insertBy066(ww25, ww2600, ww27, ww2800, ww29) → new_insertBy1(ww27, Succ(ww2800), ww29)
new_insertBy065(ww25, ww2600, ww27, ww2800, ww29, Succ(ww18100), Succ(ww14000)) → new_insertBy065(ww25, ww2600, ww27, ww2800, ww29, ww18100, ww14000)
new_insertBy01(Float(Pos(Succ(ww40000)), Neg(Succ(ww40100))), Float(Neg(Zero), Pos(Succ(Zero))), ww41) → new_insertBy6(ww41)
new_insertBy059(ww25, ww2600, ww27, ww2800, ww29, Succ(Succ(ww17900)), Zero) → new_insertBy064(ww25, ww2600, ww27, ww2800, ww29)
new_insertBy069(ww38, ww3900, ww40, ww4100, ww42, Succ(ww2620)) → new_insertBy4(ww40, Succ(ww4100), ww42)
new_insertBy075(ww44, ww4500, ww46, ww4700, ww48, Succ(ww32000), Succ(Succ(ww35900))) → new_insertBy079(ww44, ww4500, ww46, ww4700, ww48, ww32000, ww35900)
new_insertBy01(Float(Neg(Zero), Pos(Succ(ww40100))), Float(Pos(Zero), Neg(Succ(Succ(Zero)))), ww41) → new_insertBy031(ww40100, ww41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(ww40100)), Succ(ww40100)))
new_insertBy01(Float(Pos(Succ(ww40000)), Neg(Succ(ww40100))), Float(Pos(Zero), Pos(Succ(Succ(Zero)))), ww41) → new_insertBy012(ww40000, ww40100, ww41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(ww40100)), Succ(ww40100)))
new_insertBy01(Float(Pos(Zero), Pos(Succ(ww40100))), Float(Pos(Succ(ww3000)), Neg(Succ(Succ(Succ(ww310000))))), ww41) → new_insertBy09(ww40100, ww3000, ww310000, ww41, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat1(ww310000, ww40100), Succ(ww40100)), Succ(ww40100)), Succ(ww40100)))
new_insertBy6(:(ww410, ww411)) → new_insertBy01(ww410, Float(Neg(Zero), Pos(Succ(Zero))), ww411)
new_insertBy00(ww19, ww2000, ww21, ww2200, ww23, Succ(ww5600), Succ(Succ(ww8800))) → new_insertBy05(ww19, ww2000, ww21, ww2200, ww23, ww5600, ww8800)
new_insertBy045(ww44, Pos(ww450), ww46, Neg(ww470), :(ww480, ww481), Succ(ww3200)) → new_insertBy01(ww480, Float(Neg(Succ(ww46)), Neg(ww470)), ww481)
new_insertBy01(Float(Pos(Zero), Pos(Succ(ww40100))), Float(Neg(Zero), Neg(Succ(Succ(Zero)))), ww41) → new_insertBy044(ww40100, ww41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(ww40100)), Succ(ww40100)))
new_insertBy01(Float(Neg(Zero), Pos(Succ(ww40100))), Float(Pos(Succ(ww3000)), Neg(Succ(Zero))), ww41) → new_insertBy1(ww3000, Succ(Zero), ww41)
new_insertBy025(ww40000, ww40100, ww41, Succ(ww1930)) → new_insertBy058(Float(Neg(Succ(ww40000)), Neg(Succ(ww40100))), ww41)
new_insertBy01(Float(Pos(Zero), Neg(Succ(ww40100))), Float(Neg(Succ(ww3000)), Pos(Succ(Succ(Zero)))), ww41) → new_insertBy034(ww40100, ww3000, ww41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(ww40100)), Succ(ww40100)))
new_insertBy01(Float(Pos(Zero), Neg(Succ(ww40100))), Float(Pos(Succ(ww3000)), Pos(Succ(Zero))), ww41) → new_insertBy(ww3000, Succ(Zero), ww41)
new_insertBy01(Float(Neg(Succ(ww40000)), ww401), Float(Neg(Succ(ww3000)), ww31), ww41) → new_insertBy045(ww40000, ww401, ww3000, ww31, ww41, new_primPlusNat0(new_primMulNat1(ww3000, ww40000), Succ(ww40000)))
new_insertBy063(ww25, ww2600, ww27, ww2800, ww29, Succ(ww17900), Succ(ww14000)) → new_insertBy063(ww25, ww2600, ww27, ww2800, ww29, ww17900, ww14000)
new_insertBy01(Float(Pos(Succ(ww40000)), Neg(Succ(ww40100))), Float(Pos(Zero), Pos(Succ(Zero))), :(ww410, ww411)) → new_insertBy01(ww410, Float(Pos(Zero), Pos(Succ(Zero))), ww411)
new_insertBy019(ww25, Pos(Succ(ww2600)), ww27, Neg(Succ(ww2800)), ww29, Zero) → new_insertBy062(ww25, ww2600, ww27, ww2800, ww29, new_primPlusNat0(new_primMulNat1(ww2800, ww2600), Succ(ww2600)))
new_insertBy065(ww25, ww2600, ww27, ww2800, ww29, Succ(ww18100), Zero) → new_insertBy066(ww25, ww2600, ww27, ww2800, ww29)
new_insertBy041(ww40100, ww310000, ww41, Succ(ww3020)) → new_insertBy11(ww310000, ww41)
new_insertBy040(ww40000, ww40100, ww41, Succ(ww2880)) → new_insertBy14(ww41)
new_insertBy01(Float(Pos(Succ(ww40000)), Pos(Succ(ww40100))), Float(Pos(Zero), Neg(Succ(Zero))), :(ww410, ww411)) → new_insertBy01(ww410, Float(Pos(Zero), Neg(Succ(Zero))), ww411)
new_insertBy020(ww40100, ww3000, ww310000, ww41, Succ(ww1530)) → new_insertBy(ww3000, Succ(Succ(Succ(ww310000))), ww41)
new_insertBy14(:(ww410, ww411)) → new_insertBy01(ww410, Float(Neg(Zero), Neg(Succ(Succ(Zero)))), ww411)
new_insertBy01(Float(Neg(Zero), Neg(Succ(ww40100))), Float(Pos(Zero), Pos(Succ(Succ(Succ(ww310000))))), ww41) → new_insertBy028(ww40100, ww310000, ww41, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat1(ww310000, ww40100), Succ(ww40100)), Succ(ww40100)), Succ(ww40100)))
new_insertBy057(ww40100, ww41, Succ(ww4040)) → new_insertBy14(ww41)
new_insertBy01(Float(Neg(Zero), Pos(Succ(ww40100))), Float(Neg(Zero), Neg(Succ(Succ(Zero)))), ww41) → new_insertBy057(ww40100, ww41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(ww40100)), Succ(ww40100)))
new_insertBy080(ww44, ww4500, ww46, ww4700, ww48) → new_insertBy4(ww46, Succ(ww4700), ww48)
new_insertBy01(Float(Pos(Succ(ww40000)), Pos(Succ(ww40100))), Float(Pos(Zero), Neg(Succ(Succ(Zero)))), ww41) → new_insertBy014(ww40000, ww40100, ww41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(ww40100)), Succ(ww40100)))
new_insertBy074(ww38, ww3900, ww40, ww4100, ww42) → new_insertBy5(ww40, Succ(ww4100), ww42)
new_insertBy045(ww44, Neg(Succ(ww4500)), ww46, Pos(Succ(ww4700)), ww48, Zero) → new_insertBy077(ww44, ww4500, ww46, ww4700, ww48, new_primPlusNat0(new_primMulNat1(ww4700, ww4500), Succ(ww4500)))
new_insertBy021(ww40100, ww3000, ww41, Succ(ww1570)) → new_insertBy(ww3000, Succ(Succ(Zero)), ww41)
new_insertBy064(ww25, ww2600, ww27, ww2800, ww29) → new_insertBy(ww27, Succ(ww2800), ww29)
new_insertBy0(ww19, Neg(Succ(ww2000)), ww21, Pos(Succ(ww2200)), ww23, Zero) → new_insertBy03(ww19, ww2000, ww21, ww2200, ww23, new_primPlusNat0(new_primMulNat1(ww2200, ww2000), Succ(ww2000)))
new_insertBy01(Float(Neg(Zero), Neg(Succ(ww40100))), Float(Neg(Zero), Pos(Succ(Zero))), ww41) → new_insertBy6(ww41)
new_insertBy0(ww19, Neg(Zero), ww21, Neg(Succ(ww2200)), ww23, Succ(ww560)) → new_insertBy1(ww21, Succ(ww2200), ww23)
new_insertBy01(Float(Pos(Zero), Neg(Succ(ww40100))), Float(Neg(Succ(ww3000)), Pos(Succ(Succ(Succ(ww310000))))), ww41) → new_insertBy033(ww40100, ww3000, ww310000, ww41, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat1(ww310000, ww40100), Succ(ww40100)), Succ(ww40100)), Succ(ww40100)))
new_insertBy01(Float(Neg(Zero), Neg(Succ(ww40100))), Float(Neg(Succ(ww3000)), Pos(Succ(Succ(Zero)))), ww41) → new_insertBy047(ww40100, ww3000, ww41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(ww40100)), Succ(ww40100)))
new_insertBy01(Float(Neg(Zero), Neg(Succ(ww40100))), Float(Neg(Zero), Pos(Succ(Succ(Zero)))), ww41) → new_insertBy055(ww40100, ww41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(ww40100)), Succ(ww40100)))
new_insertBy01(Float(Pos(Zero), Neg(Succ(ww40100))), Float(Pos(Succ(ww3000)), Pos(Succ(Succ(Succ(ww310000))))), ww41) → new_insertBy07(ww40100, ww3000, ww310000, ww41, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat1(ww310000, ww40100), Succ(ww40100)), Succ(ww40100)), Succ(ww40100)))
new_insertBy019(ww25, Pos(Succ(ww2600)), ww27, Neg(Succ(ww2800)), ww29, Succ(ww1400)) → new_insertBy060(ww25, ww2600, ww27, ww2800, ww29, new_primPlusNat0(new_primMulNat1(ww2800, ww2600), Succ(ww2600)), ww1400)
new_insertBy0(ww19, Neg(Zero), ww21, Neg(Zero), ww23, Succ(ww560)) → new_insertBy1(ww21, Zero, ww23)
new_insertBy031(ww40100, ww41, Succ(ww2230)) → new_insertBy10(ww41)
new_insertBy084(ww44, ww4500, ww46, ww4700, ww48) → new_insertBy5(ww46, Succ(ww4700), ww48)
new_insertBy046(ww40100, ww3000, ww310000, ww41, Succ(ww3330)) → new_insertBy4(ww3000, Succ(Succ(Succ(ww310000))), ww41)
new_insertBy058(ww413, :(ww4140, ww4141)) → new_insertBy01(ww4140, Float(Pos(Zero), Pos(Succ(Succ(Zero)))), ww4141)
new_insertBy01(Float(Neg(Zero), Pos(Succ(ww40100))), Float(Pos(Succ(ww3000)), Neg(Succ(Succ(Zero)))), ww41) → new_insertBy023(ww40100, ww3000, ww41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(ww40100)), Succ(ww40100)))
new_insertBy01(Float(Neg(Succ(ww40000)), Pos(Succ(ww40100))), Float(Pos(Zero), Neg(Succ(Succ(Succ(ww310000))))), ww41) → new_insertBy026(ww40000, ww40100, ww310000, ww41, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat1(ww310000, ww40100), Succ(ww40100)), Succ(ww40100)), Succ(ww40100)))
new_insertBy023(ww40100, ww3000, ww41, Succ(ww1630)) → new_insertBy1(ww3000, Succ(Succ(Zero)), ww41)
new_insertBy053(ww40000, ww40100, :(ww410, ww411), Succ(ww3800)) → new_insertBy01(ww410, Float(Neg(Zero), Neg(Succ(Succ(Zero)))), ww411)
new_insertBy01(Float(Pos(Zero), Neg(Succ(ww40100))), Float(Pos(Zero), Pos(Succ(Zero))), ww41) → new_insertBy2(ww41)
new_insertBy013(ww40000, ww40100, ww310000, :(ww410, ww411), Succ(ww1040)) → new_insertBy01(ww410, Float(Pos(Zero), Neg(Succ(Succ(Succ(ww310000))))), ww411)
new_insertBy12(:(ww410, ww411)) → new_insertBy01(ww410, Float(Neg(Zero), Pos(Succ(Succ(Zero)))), ww411)
new_insertBy078(ww44, ww4500, ww46, ww4700, ww48, Succ(ww3550)) → new_insertBy082(ww44, Succ(ww4500), ww46, Succ(ww4700), ww48)
new_insertBy5(ww46, ww470, :(ww480, ww481)) → new_insertBy01(ww480, Float(Neg(Succ(ww46)), Neg(ww470)), ww481)
new_insertBy07(ww40100, ww3000, ww310000, ww41, Succ(ww620)) → new_insertBy(ww3000, Succ(Succ(Succ(ww310000))), ww41)
new_insertBy032(ww38, Pos(Succ(ww3900)), ww40, Neg(Succ(ww4100)), ww42, Succ(ww2310)) → new_insertBy068(ww38, ww3900, ww40, ww4100, ww42, new_primPlusNat0(new_primMulNat1(ww4100, ww3900), Succ(ww3900)), ww2310)
new_insertBy01(Float(Neg(Zero), Neg(Succ(ww40100))), Float(Neg(Zero), Pos(Succ(Succ(Succ(ww310000))))), ww41) → new_insertBy054(ww40100, ww310000, ww41, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat1(ww310000, ww40100), Succ(ww40100)), Succ(ww40100)), Succ(ww40100)))
new_insertBy01(Float(Neg(Succ(ww40000)), Neg(Succ(ww40100))), Float(Neg(Zero), Pos(Succ(Succ(Succ(ww310000))))), ww41) → new_insertBy050(ww40000, ww40100, ww310000, ww41, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat1(ww310000, ww40100), Succ(ww40100)), Succ(ww40100)), Succ(ww40100)))
new_insertBy01(Float(Pos(Zero), Neg(Succ(ww40100))), Float(Neg(Succ(ww3000)), Pos(Succ(Zero))), ww41) → new_insertBy4(ww3000, Succ(Zero), ww41)
new_insertBy043(ww40100, ww310000, ww41, Succ(ww3080)) → new_insertBy13(ww310000, ww41)
new_insertBy01(Float(Pos(Zero), Neg(Succ(ww40100))), Float(Pos(Zero), Pos(Succ(Succ(Zero)))), ww41) → new_insertBy016(ww40100, ww41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(ww40100)), Succ(ww40100)))
new_insertBy01(Float(Neg(Succ(ww40000)), Neg(Succ(ww40100))), Float(Neg(Zero), Pos(Succ(Zero))), :(ww410, ww411)) → new_insertBy01(ww410, Float(Neg(Zero), Pos(Succ(Zero))), ww411)
new_insertBy063(ww25, ww2600, ww27, ww2800, ww29, Succ(ww17900), Zero) → new_insertBy064(ww25, ww2600, ww27, ww2800, ww29)
new_insertBy081(ww44, ww450, ww46, ww470, :(ww480, ww481)) → new_insertBy01(ww480, Float(Neg(Succ(ww46)), Pos(ww470)), ww481)
new_insertBy029(ww40100, ww41, Succ(ww2170)) → new_insertBy058(Float(Neg(Zero), Neg(Succ(ww40100))), ww41)
new_insertBy061(ww25, ww2600, ww27, ww2800, ww29, Succ(ww1730)) → new_insertBy(ww27, Succ(ww2800), ww29)
new_insertBy01(Float(Neg(Zero), Pos(Succ(ww40100))), Float(Neg(Succ(ww3000)), Neg(Succ(Succ(Succ(ww310000))))), ww41) → new_insertBy048(ww40100, ww3000, ww310000, ww41, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat1(ww310000, ww40100), Succ(ww40100)), Succ(ww40100)), Succ(ww40100)))
new_insertBy0(ww19, Neg(ww200), ww21, Pos(ww220), :(ww230, ww231), Succ(ww560)) → new_insertBy01(ww230, Float(Pos(Succ(ww21)), Pos(ww220)), ww231)
new_insertBy075(ww44, ww4500, ww46, ww4700, ww48, ww3200, Zero) → new_insertBy4(ww46, Succ(ww4700), ww48)
new_insertBy082(ww44, ww450, ww46, ww470, :(ww480, ww481)) → new_insertBy01(ww480, Float(Neg(Succ(ww46)), Neg(ww470)), ww481)
new_insertBy047(ww40100, ww3000, ww41, Succ(ww3370)) → new_insertBy4(ww3000, Succ(Succ(Zero)), ww41)
new_insertBy067(ww38, ww3900, ww40, ww4100, ww42, Succ(Succ(ww26800)), Succ(ww23100)) → new_insertBy071(ww38, ww3900, ww40, ww4100, ww42, ww26800, ww23100)
new_insertBy045(ww44, Neg(ww450), ww46, Pos(ww470), :(ww480, ww481), Succ(ww3200)) → new_insertBy01(ww480, Float(Neg(Succ(ww46)), Pos(ww470)), ww481)
new_insertBy060(ww25, ww2600, ww27, ww2800, ww29, Succ(Succ(ww18100)), Succ(ww14000)) → new_insertBy065(ww25, ww2600, ww27, ww2800, ww29, ww18100, ww14000)
new_insertBy060(ww25, ww2600, ww27, ww2800, ww29, Succ(Succ(ww18100)), Zero) → new_insertBy066(ww25, ww2600, ww27, ww2800, ww29)
new_insertBy045(ww44, Pos(Succ(ww4500)), ww46, Pos(Succ(ww4700)), ww48, Succ(ww3200)) → new_insertBy075(ww44, ww4500, ww46, ww4700, ww48, ww3200, new_primPlusNat0(new_primMulNat1(ww4700, ww4500), Succ(ww4500)))
new_insertBy035(ww40100, ww3000, ww310000, ww41, Succ(ww2480)) → new_insertBy5(ww3000, Succ(Succ(Succ(ww310000))), ww41)
new_insertBy068(ww38, ww3900, ww40, ww4100, ww42, Succ(Succ(ww27000)), Zero) → new_insertBy074(ww38, ww3900, ww40, ww4100, ww42)
new_insertBy01(Float(Pos(Succ(ww40000)), Pos(Succ(ww40100))), Float(Pos(Zero), Neg(Succ(Succ(Succ(ww310000))))), ww41) → new_insertBy013(ww40000, ww40100, ww310000, ww41, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat1(ww310000, ww40100), Succ(ww40100)), Succ(ww40100)), Succ(ww40100)))
new_insertBy01(Float(Pos(Zero), Pos(Succ(ww40100))), Float(Neg(Zero), Neg(Succ(Zero))), ww41) → new_insertBy7(ww41)
new_insertBy01(Float(Neg(Succ(ww40000)), Neg(Succ(ww40100))), Float(Pos(Zero), Pos(Succ(Zero))), ww41) → new_insertBy2(ww41)
new_insertBy045(ww44, Pos(Zero), ww46, Pos(Succ(ww4700)), ww48, Succ(ww3200)) → new_insertBy4(ww46, Succ(ww4700), ww48)
new_insertBy071(ww38, ww3900, ww40, ww4100, ww42, Succ(ww26800), Zero) → new_insertBy072(ww38, ww3900, ww40, ww4100, ww42)
new_insertBy042(ww40100, ww41, Succ(ww3060)) → new_insertBy12(ww41)
new_insertBy05(ww19, ww2000, ww21, ww2200, ww23, Succ(ww5600), Zero) → new_insertBy06(ww19, ww2000, ww21, ww2200, ww23)
new_insertBy01(Float(Pos(Succ(ww40000)), Pos(Succ(ww40100))), Float(Neg(Zero), Neg(Succ(Succ(Succ(ww310000))))), ww41) → new_insertBy039(ww40000, ww40100, ww310000, ww41, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat1(ww310000, ww40100), Succ(ww40100)), Succ(ww40100)), Succ(ww40100)))
new_insertBy072(ww38, ww3900, ww40, ww4100, ww42) → new_insertBy4(ww40, Succ(ww4100), ww42)
new_insertBy030(ww40100, ww310000, ww41, Succ(ww2190)) → new_insertBy9(ww310000, ww41)
new_insertBy01(Float(Neg(Zero), Pos(Succ(ww40100))), Float(Pos(Zero), Neg(Succ(Succ(Succ(ww310000))))), ww41) → new_insertBy030(ww40100, ww310000, ww41, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat1(ww310000, ww40100), Succ(ww40100)), Succ(ww40100)), Succ(ww40100)))
new_insertBy01(Float(Neg(Zero), Neg(Succ(ww40100))), Float(Pos(Zero), Pos(Succ(Zero))), ww41) → new_insertBy2(ww41)
new_insertBy0(ww19, Pos(Zero), ww21, Pos(Succ(ww2200)), ww23, Succ(ww560)) → new_insertBy(ww21, Succ(ww2200), ww23)
new_insertBy033(ww40100, ww3000, ww310000, ww41, Succ(ww2420)) → new_insertBy4(ww3000, Succ(Succ(Succ(ww310000))), ww41)
new_insertBy01(Float(Neg(Succ(ww40000)), Neg(Succ(ww40100))), Float(Neg(Zero), Pos(Succ(Succ(Zero)))), ww41) → new_insertBy051(ww40000, ww40100, ww41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(ww40100)), Succ(ww40100)))
new_insertBy050(ww40000, ww40100, ww310000, :(ww410, ww411), Succ(ww3700)) → new_insertBy01(ww410, Float(Neg(Zero), Pos(Succ(Succ(Succ(ww310000))))), ww411)
new_insertBy038(ww40000, ww40100, ww41, Succ(ww2820)) → new_insertBy12(ww41)
new_insertBy01(Float(Neg(Succ(ww40000)), Pos(Succ(ww40100))), Float(Pos(Zero), Neg(Succ(Zero))), ww41) → new_insertBy3(ww41)
new_insertBy068(ww38, ww3900, ww40, ww4100, ww42, Succ(Succ(ww27000)), Succ(ww23100)) → new_insertBy073(ww38, ww3900, ww40, ww4100, ww42, ww27000, ww23100)
new_insertBy01(Float(Neg(Zero), Pos(Succ(ww40100))), Float(Neg(Succ(ww3000)), Neg(Succ(Zero))), ww41) → new_insertBy5(ww3000, Succ(Zero), ww41)
new_insertBy054(ww40100, ww310000, ww41, Succ(ww3940)) → new_insertBy11(ww310000, ww41)
new_insertBy01(Float(Pos(Succ(ww40000)), ww401), Float(Neg(Succ(ww3000)), ww31), ww41) → new_insertBy032(ww40000, ww401, ww3000, ww31, ww41, new_primPlusNat0(new_primMulNat1(ww3000, ww40000), Succ(ww40000)))
new_insertBy071(ww38, ww3900, ww40, ww4100, ww42, Succ(ww26800), Succ(ww23100)) → new_insertBy071(ww38, ww3900, ww40, ww4100, ww42, ww26800, ww23100)
new_insertBy01(Float(Pos(Zero), Neg(Succ(ww40100))), Float(Neg(Zero), Pos(Succ(Succ(Succ(ww310000))))), ww41) → new_insertBy041(ww40100, ww310000, ww41, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat1(ww310000, ww40100), Succ(ww40100)), Succ(ww40100)), Succ(ww40100)))
new_insertBy02(ww19, ww2000, ww21, ww2200, ww23, ww560, Zero) → new_insertBy1(ww21, Succ(ww2200), ww23)
new_insertBy055(ww40100, ww41, Succ(ww3980)) → new_insertBy12(ww41)
new_insertBy032(ww38, Neg(Succ(ww3900)), ww40, Pos(Succ(ww4100)), ww42, Succ(ww2310)) → new_insertBy067(ww38, ww3900, ww40, ww4100, ww42, new_primPlusNat0(new_primMulNat1(ww4100, ww3900), Succ(ww3900)), ww2310)
new_insertBy049(ww40100, ww3000, ww41, Succ(ww3430)) → new_insertBy5(ww3000, Succ(Succ(Zero)), ww41)
new_insertBy048(ww40100, ww3000, ww310000, ww41, Succ(ww3390)) → new_insertBy5(ww3000, Succ(Succ(Succ(ww310000))), ww41)
new_insertBy01(Float(Pos(Zero), Pos(Succ(ww40100))), Float(Pos(Succ(ww3000)), Neg(Succ(Zero))), ww41) → new_insertBy1(ww3000, Succ(Zero), ww41)
new_insertBy03(ww19, ww2000, ww21, ww2200, ww23, Succ(ww820)) → new_insertBy085(ww19, Succ(ww2000), ww21, Succ(ww2200), ww23)
new_insertBy01(Float(Neg(Zero), Pos(Succ(ww40100))), Float(Pos(Zero), Neg(Succ(Zero))), ww41) → new_insertBy3(ww41)
new_insertBy04(ww19, ww2000, ww21, ww2200, ww23, Succ(ww840)) → new_insertBy086(ww19, Succ(ww2000), ww21, Succ(ww2200), ww23)
new_insertBy011(ww40000, ww40100, ww310000, :(ww410, ww411), Succ(ww980)) → new_insertBy01(ww410, Float(Pos(Zero), Pos(Succ(Succ(Succ(ww310000))))), ww411)
new_insertBy11(ww310000, :(ww410, ww411)) → new_insertBy01(ww410, Float(Neg(Zero), Pos(Succ(Succ(Succ(ww310000))))), ww411)
new_insertBy076(ww44, ww4500, ww46, ww4700, ww48, Succ(ww32000), Succ(Succ(ww36100))) → new_insertBy083(ww44, ww4500, ww46, ww4700, ww48, ww32000, ww36100)
new_insertBy0(ww19, Pos(Succ(ww2000)), ww21, Pos(Succ(ww2200)), ww23, Succ(ww560)) → new_insertBy00(ww19, ww2000, ww21, ww2200, ww23, ww560, new_primPlusNat0(new_primMulNat1(ww2200, ww2000), Succ(ww2000)))
new_insertBy01(Float(Neg(Zero), Neg(Succ(ww40100))), Float(Pos(Succ(ww3000)), Pos(Succ(Zero))), ww41) → new_insertBy(ww3000, Succ(Zero), ww41)
new_insertBy077(ww44, ww4500, ww46, ww4700, ww48, Succ(ww3530)) → new_insertBy081(ww44, Succ(ww4500), ww46, Succ(ww4700), ww48)
new_insertBy02(ww19, ww2000, ww21, ww2200, ww23, Succ(ww5600), Succ(Succ(ww9000))) → new_insertBy087(ww19, ww2000, ww21, ww2200, ww23, ww5600, ww9000)
new_insertBy1(ww21, ww220, :(ww230, ww231)) → new_insertBy01(ww230, Float(Pos(Succ(ww21)), Neg(ww220)), ww231)
new_insertBy01(Float(Neg(Succ(ww40000)), Pos(Succ(ww40100))), Float(Neg(Zero), Neg(Succ(Succ(Succ(ww310000))))), ww41) → new_insertBy052(ww40000, ww40100, ww310000, ww41, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat1(ww310000, ww40100), Succ(ww40100)), Succ(ww40100)), Succ(ww40100)))
new_insertBy073(ww38, ww3900, ww40, ww4100, ww42, Succ(ww27000), Succ(ww23100)) → new_insertBy073(ww38, ww3900, ww40, ww4100, ww42, ww27000, ww23100)
new_insertBy073(ww38, ww3900, ww40, ww4100, ww42, Succ(ww27000), Zero) → new_insertBy074(ww38, ww3900, ww40, ww4100, ww42)
new_insertBy09(ww40100, ww3000, ww310000, ww41, Succ(ww680)) → new_insertBy1(ww3000, Succ(Succ(Succ(ww310000))), ww41)
new_insertBy01(Float(Neg(Succ(ww40000)), ww401), Float(Pos(Succ(ww3000)), ww31), ww41) → new_insertBy019(ww40000, ww401, ww3000, ww31, ww41, new_primPlusNat0(new_primMulNat1(ww3000, ww40000), Succ(ww40000)))
new_insertBy01(Float(Neg(Zero), Pos(Succ(ww40100))), Float(Neg(Zero), Neg(Succ(Zero))), ww41) → new_insertBy7(ww41)
new_insertBy9(ww310000, :(ww410, ww411)) → new_insertBy01(ww410, Float(Pos(Zero), Neg(Succ(Succ(Succ(ww310000))))), ww411)
new_insertBy067(ww38, ww3900, ww40, ww4100, ww42, Succ(Succ(ww26800)), Zero) → new_insertBy072(ww38, ww3900, ww40, ww4100, ww42)
new_insertBy01(Float(Pos(Succ(ww40000)), Pos(Succ(ww40100))), Float(Neg(Zero), Neg(Succ(Zero))), ww41) → new_insertBy7(ww41)
new_insertBy016(ww40100, ww41, Succ(ww1260)) → new_insertBy058(Float(Pos(Zero), Neg(Succ(ww40100))), ww41)
new_insertBy(ww21, ww220, :(ww230, ww231)) → new_insertBy01(ww230, Float(Pos(Succ(ww21)), Pos(ww220)), ww231)
new_insertBy028(ww40100, ww310000, ww41, Succ(ww2130)) → new_insertBy8(ww310000, ww41)
new_insertBy01(Float(Neg(Zero), Neg(Succ(ww40100))), Float(Pos(Zero), Pos(Succ(Succ(Zero)))), ww41) → new_insertBy029(ww40100, ww41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(ww40100)), Succ(ww40100)))
new_insertBy01(Float(Pos(Succ(ww40000)), ww401), Float(Pos(Succ(ww3000)), ww31), ww41) → new_insertBy0(ww40000, ww401, ww3000, ww31, ww41, new_primPlusNat1(new_primMulNat1(ww3000, ww40000), ww40000))

The TRS R consists of the following rules:

new_primPlusNat1(Zero, ww40000) → Succ(ww40000)
new_primPlusNat0(Zero, Zero) → Zero
new_primMulNat1(Zero, ww40000) → Zero
new_primPlusNat1(Succ(ww550), ww40000) → Succ(Succ(new_primPlusNat0(ww550, ww40000)))
new_primPlusNat0(Succ(ww5500), Zero) → Succ(ww5500)
new_primPlusNat0(Zero, Succ(ww400000)) → Succ(ww400000)
new_primPlusNat0(Succ(ww5500), Succ(ww400000)) → Succ(Succ(new_primPlusNat0(ww5500, ww400000)))
new_primMulNat1(Succ(ww30000), ww40000) → new_primPlusNat1(new_primMulNat1(ww30000, ww40000), ww40000)

The set Q consists of the following terms:

new_primPlusNat0(Succ(x0), Succ(x1))
new_primPlusNat0(Zero, Zero)
new_primPlusNat0(Zero, Succ(x0))
new_primPlusNat0(Succ(x0), Zero)
new_primPlusNat1(Succ(x0), x1)
new_primMulNat1(Zero, x0)
new_primPlusNat1(Zero, x0)
new_primMulNat1(Succ(x0), x1)

We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 14 SCCs.

↳ HASKELL
  ↳ CR
    ↳ HASKELL
      ↳ BR
        ↳ HASKELL
          ↳ COR
            ↳ HASKELL
              ↳ Narrow
                ↳ AND
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                    ↳ DependencyGraphProof
                      ↳ AND
QDP
                          ↳ UsableRulesProof
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_insertBy01(Float(Neg(Succ(ww40000)), Neg(Succ(ww40100))), Float(Pos(Zero), Pos(Succ(Zero))), ww41) → new_insertBy2(ww41)
new_insertBy2(:(ww410, ww411)) → new_insertBy01(ww410, Float(Pos(Zero), Pos(Succ(Zero))), ww411)
new_insertBy01(Float(Pos(Succ(ww40000)), Neg(Succ(ww40100))), Float(Pos(Zero), Pos(Succ(Zero))), :(ww410, ww411)) → new_insertBy01(ww410, Float(Pos(Zero), Pos(Succ(Zero))), ww411)
new_insertBy01(Float(Neg(Zero), Neg(Succ(ww40100))), Float(Pos(Zero), Pos(Succ(Zero))), ww41) → new_insertBy2(ww41)
new_insertBy01(Float(Pos(Zero), Neg(Succ(ww40100))), Float(Pos(Zero), Pos(Succ(Zero))), ww41) → new_insertBy2(ww41)

The TRS R consists of the following rules:

new_primPlusNat1(Zero, ww40000) → Succ(ww40000)
new_primPlusNat0(Zero, Zero) → Zero
new_primMulNat1(Zero, ww40000) → Zero
new_primPlusNat1(Succ(ww550), ww40000) → Succ(Succ(new_primPlusNat0(ww550, ww40000)))
new_primPlusNat0(Succ(ww5500), Zero) → Succ(ww5500)
new_primPlusNat0(Zero, Succ(ww400000)) → Succ(ww400000)
new_primPlusNat0(Succ(ww5500), Succ(ww400000)) → Succ(Succ(new_primPlusNat0(ww5500, ww400000)))
new_primMulNat1(Succ(ww30000), ww40000) → new_primPlusNat1(new_primMulNat1(ww30000, ww40000), ww40000)

The set Q consists of the following terms:

new_primPlusNat0(Succ(x0), Succ(x1))
new_primPlusNat0(Zero, Zero)
new_primPlusNat0(Zero, Succ(x0))
new_primPlusNat0(Succ(x0), Zero)
new_primPlusNat1(Succ(x0), x1)
new_primMulNat1(Zero, x0)
new_primPlusNat1(Zero, x0)
new_primMulNat1(Succ(x0), x1)

We have to consider all minimal (P,Q,R)-chains.
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [15] we can delete all non-usable rules [17] from R.

↳ HASKELL
  ↳ CR
    ↳ HASKELL
      ↳ BR
        ↳ HASKELL
          ↳ COR
            ↳ HASKELL
              ↳ Narrow
                ↳ AND
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                    ↳ DependencyGraphProof
                      ↳ AND
                        ↳ QDP
                          ↳ UsableRulesProof
QDP
                              ↳ QReductionProof
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_insertBy01(Float(Neg(Succ(ww40000)), Neg(Succ(ww40100))), Float(Pos(Zero), Pos(Succ(Zero))), ww41) → new_insertBy2(ww41)
new_insertBy2(:(ww410, ww411)) → new_insertBy01(ww410, Float(Pos(Zero), Pos(Succ(Zero))), ww411)
new_insertBy01(Float(Pos(Succ(ww40000)), Neg(Succ(ww40100))), Float(Pos(Zero), Pos(Succ(Zero))), :(ww410, ww411)) → new_insertBy01(ww410, Float(Pos(Zero), Pos(Succ(Zero))), ww411)
new_insertBy01(Float(Neg(Zero), Neg(Succ(ww40100))), Float(Pos(Zero), Pos(Succ(Zero))), ww41) → new_insertBy2(ww41)
new_insertBy01(Float(Pos(Zero), Neg(Succ(ww40100))), Float(Pos(Zero), Pos(Succ(Zero))), ww41) → new_insertBy2(ww41)

R is empty.
The set Q consists of the following terms:

new_primPlusNat0(Succ(x0), Succ(x1))
new_primPlusNat0(Zero, Zero)
new_primPlusNat0(Zero, Succ(x0))
new_primPlusNat0(Succ(x0), Zero)
new_primPlusNat1(Succ(x0), x1)
new_primMulNat1(Zero, x0)
new_primPlusNat1(Zero, x0)
new_primMulNat1(Succ(x0), x1)

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.

new_primPlusNat0(Succ(x0), Succ(x1))
new_primPlusNat0(Zero, Zero)
new_primPlusNat0(Zero, Succ(x0))
new_primPlusNat0(Succ(x0), Zero)
new_primPlusNat1(Succ(x0), x1)
new_primMulNat1(Zero, x0)
new_primPlusNat1(Zero, x0)
new_primMulNat1(Succ(x0), x1)



↳ HASKELL
  ↳ CR
    ↳ HASKELL
      ↳ BR
        ↳ HASKELL
          ↳ COR
            ↳ HASKELL
              ↳ Narrow
                ↳ AND
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                    ↳ DependencyGraphProof
                      ↳ AND
                        ↳ QDP
                          ↳ UsableRulesProof
                            ↳ QDP
                              ↳ QReductionProof
QDP
                                  ↳ QDPSizeChangeProof
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_insertBy2(:(ww410, ww411)) → new_insertBy01(ww410, Float(Pos(Zero), Pos(Succ(Zero))), ww411)
new_insertBy01(Float(Neg(Succ(ww40000)), Neg(Succ(ww40100))), Float(Pos(Zero), Pos(Succ(Zero))), ww41) → new_insertBy2(ww41)
new_insertBy01(Float(Pos(Succ(ww40000)), Neg(Succ(ww40100))), Float(Pos(Zero), Pos(Succ(Zero))), :(ww410, ww411)) → new_insertBy01(ww410, Float(Pos(Zero), Pos(Succ(Zero))), ww411)
new_insertBy01(Float(Neg(Zero), Neg(Succ(ww40100))), Float(Pos(Zero), Pos(Succ(Zero))), ww41) → new_insertBy2(ww41)
new_insertBy01(Float(Pos(Zero), Neg(Succ(ww40100))), Float(Pos(Zero), Pos(Succ(Zero))), ww41) → new_insertBy2(ww41)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ CR
    ↳ HASKELL
      ↳ BR
        ↳ HASKELL
          ↳ COR
            ↳ HASKELL
              ↳ Narrow
                ↳ AND
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                    ↳ DependencyGraphProof
                      ↳ AND
                        ↳ QDP
QDP
                          ↳ UsableRulesProof
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_insertBy6(:(ww410, ww411)) → new_insertBy01(ww410, Float(Neg(Zero), Pos(Succ(Zero))), ww411)
new_insertBy01(Float(Neg(Zero), Neg(Succ(ww40100))), Float(Neg(Zero), Pos(Succ(Zero))), ww41) → new_insertBy6(ww41)
new_insertBy01(Float(Pos(Zero), Neg(Succ(ww40100))), Float(Neg(Zero), Pos(Succ(Zero))), ww41) → new_insertBy6(ww41)
new_insertBy01(Float(Pos(Succ(ww40000)), Neg(Succ(ww40100))), Float(Neg(Zero), Pos(Succ(Zero))), ww41) → new_insertBy6(ww41)
new_insertBy01(Float(Neg(Succ(ww40000)), Neg(Succ(ww40100))), Float(Neg(Zero), Pos(Succ(Zero))), :(ww410, ww411)) → new_insertBy01(ww410, Float(Neg(Zero), Pos(Succ(Zero))), ww411)

The TRS R consists of the following rules:

new_primPlusNat1(Zero, ww40000) → Succ(ww40000)
new_primPlusNat0(Zero, Zero) → Zero
new_primMulNat1(Zero, ww40000) → Zero
new_primPlusNat1(Succ(ww550), ww40000) → Succ(Succ(new_primPlusNat0(ww550, ww40000)))
new_primPlusNat0(Succ(ww5500), Zero) → Succ(ww5500)
new_primPlusNat0(Zero, Succ(ww400000)) → Succ(ww400000)
new_primPlusNat0(Succ(ww5500), Succ(ww400000)) → Succ(Succ(new_primPlusNat0(ww5500, ww400000)))
new_primMulNat1(Succ(ww30000), ww40000) → new_primPlusNat1(new_primMulNat1(ww30000, ww40000), ww40000)

The set Q consists of the following terms:

new_primPlusNat0(Succ(x0), Succ(x1))
new_primPlusNat0(Zero, Zero)
new_primPlusNat0(Zero, Succ(x0))
new_primPlusNat0(Succ(x0), Zero)
new_primPlusNat1(Succ(x0), x1)
new_primMulNat1(Zero, x0)
new_primPlusNat1(Zero, x0)
new_primMulNat1(Succ(x0), x1)

We have to consider all minimal (P,Q,R)-chains.
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [15] we can delete all non-usable rules [17] from R.

↳ HASKELL
  ↳ CR
    ↳ HASKELL
      ↳ BR
        ↳ HASKELL
          ↳ COR
            ↳ HASKELL
              ↳ Narrow
                ↳ AND
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                    ↳ DependencyGraphProof
                      ↳ AND
                        ↳ QDP
                        ↳ QDP
                          ↳ UsableRulesProof
QDP
                              ↳ QReductionProof
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_insertBy6(:(ww410, ww411)) → new_insertBy01(ww410, Float(Neg(Zero), Pos(Succ(Zero))), ww411)
new_insertBy01(Float(Neg(Zero), Neg(Succ(ww40100))), Float(Neg(Zero), Pos(Succ(Zero))), ww41) → new_insertBy6(ww41)
new_insertBy01(Float(Pos(Zero), Neg(Succ(ww40100))), Float(Neg(Zero), Pos(Succ(Zero))), ww41) → new_insertBy6(ww41)
new_insertBy01(Float(Pos(Succ(ww40000)), Neg(Succ(ww40100))), Float(Neg(Zero), Pos(Succ(Zero))), ww41) → new_insertBy6(ww41)
new_insertBy01(Float(Neg(Succ(ww40000)), Neg(Succ(ww40100))), Float(Neg(Zero), Pos(Succ(Zero))), :(ww410, ww411)) → new_insertBy01(ww410, Float(Neg(Zero), Pos(Succ(Zero))), ww411)

R is empty.
The set Q consists of the following terms:

new_primPlusNat0(Succ(x0), Succ(x1))
new_primPlusNat0(Zero, Zero)
new_primPlusNat0(Zero, Succ(x0))
new_primPlusNat0(Succ(x0), Zero)
new_primPlusNat1(Succ(x0), x1)
new_primMulNat1(Zero, x0)
new_primPlusNat1(Zero, x0)
new_primMulNat1(Succ(x0), x1)

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.

new_primPlusNat0(Succ(x0), Succ(x1))
new_primPlusNat0(Zero, Zero)
new_primPlusNat0(Zero, Succ(x0))
new_primPlusNat0(Succ(x0), Zero)
new_primPlusNat1(Succ(x0), x1)
new_primMulNat1(Zero, x0)
new_primPlusNat1(Zero, x0)
new_primMulNat1(Succ(x0), x1)



↳ HASKELL
  ↳ CR
    ↳ HASKELL
      ↳ BR
        ↳ HASKELL
          ↳ COR
            ↳ HASKELL
              ↳ Narrow
                ↳ AND
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                    ↳ DependencyGraphProof
                      ↳ AND
                        ↳ QDP
                        ↳ QDP
                          ↳ UsableRulesProof
                            ↳ QDP
                              ↳ QReductionProof
QDP
                                  ↳ QDPSizeChangeProof
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_insertBy6(:(ww410, ww411)) → new_insertBy01(ww410, Float(Neg(Zero), Pos(Succ(Zero))), ww411)
new_insertBy01(Float(Neg(Zero), Neg(Succ(ww40100))), Float(Neg(Zero), Pos(Succ(Zero))), ww41) → new_insertBy6(ww41)
new_insertBy01(Float(Pos(Zero), Neg(Succ(ww40100))), Float(Neg(Zero), Pos(Succ(Zero))), ww41) → new_insertBy6(ww41)
new_insertBy01(Float(Pos(Succ(ww40000)), Neg(Succ(ww40100))), Float(Neg(Zero), Pos(Succ(Zero))), ww41) → new_insertBy6(ww41)
new_insertBy01(Float(Neg(Succ(ww40000)), Neg(Succ(ww40100))), Float(Neg(Zero), Pos(Succ(Zero))), :(ww410, ww411)) → new_insertBy01(ww410, Float(Neg(Zero), Pos(Succ(Zero))), ww411)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ CR
    ↳ HASKELL
      ↳ BR
        ↳ HASKELL
          ↳ COR
            ↳ HASKELL
              ↳ Narrow
                ↳ AND
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                    ↳ DependencyGraphProof
                      ↳ AND
                        ↳ QDP
                        ↳ QDP
QDP
                          ↳ QDPSizeChangeProof
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_insertBy11(ww310000, :(ww410, ww411)) → new_insertBy01(ww410, Float(Neg(Zero), Pos(Succ(Succ(Succ(ww310000))))), ww411)
new_insertBy037(ww40000, ww40100, ww310000, ww41, Succ(ww2780)) → new_insertBy11(ww310000, ww41)
new_insertBy054(ww40100, ww310000, ww41, Succ(ww3940)) → new_insertBy11(ww310000, ww41)
new_insertBy01(Float(Pos(Succ(ww40000)), Neg(Succ(ww40100))), Float(Neg(Zero), Pos(Succ(Succ(Succ(ww310000))))), ww41) → new_insertBy037(ww40000, ww40100, ww310000, ww41, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat1(ww310000, ww40100), Succ(ww40100)), Succ(ww40100)), Succ(ww40100)))
new_insertBy041(ww40100, ww310000, ww41, Succ(ww3020)) → new_insertBy11(ww310000, ww41)
new_insertBy01(Float(Pos(Zero), Neg(Succ(ww40100))), Float(Neg(Zero), Pos(Succ(Succ(Succ(ww310000))))), ww41) → new_insertBy041(ww40100, ww310000, ww41, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat1(ww310000, ww40100), Succ(ww40100)), Succ(ww40100)), Succ(ww40100)))
new_insertBy01(Float(Neg(Zero), Neg(Succ(ww40100))), Float(Neg(Zero), Pos(Succ(Succ(Succ(ww310000))))), ww41) → new_insertBy054(ww40100, ww310000, ww41, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat1(ww310000, ww40100), Succ(ww40100)), Succ(ww40100)), Succ(ww40100)))
new_insertBy01(Float(Neg(Succ(ww40000)), Neg(Succ(ww40100))), Float(Neg(Zero), Pos(Succ(Succ(Succ(ww310000))))), ww41) → new_insertBy050(ww40000, ww40100, ww310000, ww41, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat1(ww310000, ww40100), Succ(ww40100)), Succ(ww40100)), Succ(ww40100)))
new_insertBy050(ww40000, ww40100, ww310000, :(ww410, ww411), Succ(ww3700)) → new_insertBy01(ww410, Float(Neg(Zero), Pos(Succ(Succ(Succ(ww310000))))), ww411)

The TRS R consists of the following rules:

new_primPlusNat1(Zero, ww40000) → Succ(ww40000)
new_primPlusNat0(Zero, Zero) → Zero
new_primMulNat1(Zero, ww40000) → Zero
new_primPlusNat1(Succ(ww550), ww40000) → Succ(Succ(new_primPlusNat0(ww550, ww40000)))
new_primPlusNat0(Succ(ww5500), Zero) → Succ(ww5500)
new_primPlusNat0(Zero, Succ(ww400000)) → Succ(ww400000)
new_primPlusNat0(Succ(ww5500), Succ(ww400000)) → Succ(Succ(new_primPlusNat0(ww5500, ww400000)))
new_primMulNat1(Succ(ww30000), ww40000) → new_primPlusNat1(new_primMulNat1(ww30000, ww40000), ww40000)

The set Q consists of the following terms:

new_primPlusNat0(Succ(x0), Succ(x1))
new_primPlusNat0(Zero, Zero)
new_primPlusNat0(Zero, Succ(x0))
new_primPlusNat0(Succ(x0), Zero)
new_primPlusNat1(Succ(x0), x1)
new_primMulNat1(Zero, x0)
new_primPlusNat1(Zero, x0)
new_primMulNat1(Succ(x0), x1)

We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ CR
    ↳ HASKELL
      ↳ BR
        ↳ HASKELL
          ↳ COR
            ↳ HASKELL
              ↳ Narrow
                ↳ AND
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                    ↳ DependencyGraphProof
                      ↳ AND
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
QDP
                          ↳ UsableRulesProof
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_insertBy01(Float(Neg(Succ(ww40000)), Pos(Succ(ww40100))), Float(Neg(Zero), Neg(Succ(Succ(Zero)))), ww41) → new_insertBy053(ww40000, ww40100, ww41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(ww40100)), Succ(ww40100)))
new_insertBy057(ww40100, ww41, Succ(ww4040)) → new_insertBy14(ww41)
new_insertBy01(Float(Neg(Zero), Pos(Succ(ww40100))), Float(Neg(Zero), Neg(Succ(Succ(Zero)))), ww41) → new_insertBy057(ww40100, ww41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(ww40100)), Succ(ww40100)))
new_insertBy044(ww40100, ww41, Succ(ww3120)) → new_insertBy14(ww41)
new_insertBy01(Float(Pos(Zero), Pos(Succ(ww40100))), Float(Neg(Zero), Neg(Succ(Succ(Zero)))), ww41) → new_insertBy044(ww40100, ww41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(ww40100)), Succ(ww40100)))
new_insertBy040(ww40000, ww40100, ww41, Succ(ww2880)) → new_insertBy14(ww41)
new_insertBy053(ww40000, ww40100, :(ww410, ww411), Succ(ww3800)) → new_insertBy01(ww410, Float(Neg(Zero), Neg(Succ(Succ(Zero)))), ww411)
new_insertBy14(:(ww410, ww411)) → new_insertBy01(ww410, Float(Neg(Zero), Neg(Succ(Succ(Zero)))), ww411)
new_insertBy01(Float(Pos(Succ(ww40000)), Pos(Succ(ww40100))), Float(Neg(Zero), Neg(Succ(Succ(Zero)))), ww41) → new_insertBy040(ww40000, ww40100, ww41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(ww40100)), Succ(ww40100)))

The TRS R consists of the following rules:

new_primPlusNat1(Zero, ww40000) → Succ(ww40000)
new_primPlusNat0(Zero, Zero) → Zero
new_primMulNat1(Zero, ww40000) → Zero
new_primPlusNat1(Succ(ww550), ww40000) → Succ(Succ(new_primPlusNat0(ww550, ww40000)))
new_primPlusNat0(Succ(ww5500), Zero) → Succ(ww5500)
new_primPlusNat0(Zero, Succ(ww400000)) → Succ(ww400000)
new_primPlusNat0(Succ(ww5500), Succ(ww400000)) → Succ(Succ(new_primPlusNat0(ww5500, ww400000)))
new_primMulNat1(Succ(ww30000), ww40000) → new_primPlusNat1(new_primMulNat1(ww30000, ww40000), ww40000)

The set Q consists of the following terms:

new_primPlusNat0(Succ(x0), Succ(x1))
new_primPlusNat0(Zero, Zero)
new_primPlusNat0(Zero, Succ(x0))
new_primPlusNat0(Succ(x0), Zero)
new_primPlusNat1(Succ(x0), x1)
new_primMulNat1(Zero, x0)
new_primPlusNat1(Zero, x0)
new_primMulNat1(Succ(x0), x1)

We have to consider all minimal (P,Q,R)-chains.
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [15] we can delete all non-usable rules [17] from R.

↳ HASKELL
  ↳ CR
    ↳ HASKELL
      ↳ BR
        ↳ HASKELL
          ↳ COR
            ↳ HASKELL
              ↳ Narrow
                ↳ AND
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                    ↳ DependencyGraphProof
                      ↳ AND
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                          ↳ UsableRulesProof
QDP
                              ↳ QReductionProof
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_insertBy01(Float(Neg(Succ(ww40000)), Pos(Succ(ww40100))), Float(Neg(Zero), Neg(Succ(Succ(Zero)))), ww41) → new_insertBy053(ww40000, ww40100, ww41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(ww40100)), Succ(ww40100)))
new_insertBy057(ww40100, ww41, Succ(ww4040)) → new_insertBy14(ww41)
new_insertBy01(Float(Neg(Zero), Pos(Succ(ww40100))), Float(Neg(Zero), Neg(Succ(Succ(Zero)))), ww41) → new_insertBy057(ww40100, ww41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(ww40100)), Succ(ww40100)))
new_insertBy044(ww40100, ww41, Succ(ww3120)) → new_insertBy14(ww41)
new_insertBy01(Float(Pos(Zero), Pos(Succ(ww40100))), Float(Neg(Zero), Neg(Succ(Succ(Zero)))), ww41) → new_insertBy044(ww40100, ww41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(ww40100)), Succ(ww40100)))
new_insertBy040(ww40000, ww40100, ww41, Succ(ww2880)) → new_insertBy14(ww41)
new_insertBy053(ww40000, ww40100, :(ww410, ww411), Succ(ww3800)) → new_insertBy01(ww410, Float(Neg(Zero), Neg(Succ(Succ(Zero)))), ww411)
new_insertBy14(:(ww410, ww411)) → new_insertBy01(ww410, Float(Neg(Zero), Neg(Succ(Succ(Zero)))), ww411)
new_insertBy01(Float(Pos(Succ(ww40000)), Pos(Succ(ww40100))), Float(Neg(Zero), Neg(Succ(Succ(Zero)))), ww41) → new_insertBy040(ww40000, ww40100, ww41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(ww40100)), Succ(ww40100)))

The TRS R consists of the following rules:

new_primPlusNat0(Zero, Succ(ww400000)) → Succ(ww400000)
new_primPlusNat0(Succ(ww5500), Succ(ww400000)) → Succ(Succ(new_primPlusNat0(ww5500, ww400000)))
new_primPlusNat0(Zero, Zero) → Zero
new_primPlusNat0(Succ(ww5500), Zero) → Succ(ww5500)

The set Q consists of the following terms:

new_primPlusNat0(Succ(x0), Succ(x1))
new_primPlusNat0(Zero, Zero)
new_primPlusNat0(Zero, Succ(x0))
new_primPlusNat0(Succ(x0), Zero)
new_primPlusNat1(Succ(x0), x1)
new_primMulNat1(Zero, x0)
new_primPlusNat1(Zero, x0)
new_primMulNat1(Succ(x0), x1)

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.

new_primPlusNat1(Succ(x0), x1)
new_primMulNat1(Zero, x0)
new_primPlusNat1(Zero, x0)
new_primMulNat1(Succ(x0), x1)



↳ HASKELL
  ↳ CR
    ↳ HASKELL
      ↳ BR
        ↳ HASKELL
          ↳ COR
            ↳ HASKELL
              ↳ Narrow
                ↳ AND
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                    ↳ DependencyGraphProof
                      ↳ AND
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                          ↳ UsableRulesProof
                            ↳ QDP
                              ↳ QReductionProof
QDP
                                  ↳ QDPSizeChangeProof
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_insertBy01(Float(Neg(Succ(ww40000)), Pos(Succ(ww40100))), Float(Neg(Zero), Neg(Succ(Succ(Zero)))), ww41) → new_insertBy053(ww40000, ww40100, ww41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(ww40100)), Succ(ww40100)))
new_insertBy057(ww40100, ww41, Succ(ww4040)) → new_insertBy14(ww41)
new_insertBy01(Float(Pos(Zero), Pos(Succ(ww40100))), Float(Neg(Zero), Neg(Succ(Succ(Zero)))), ww41) → new_insertBy044(ww40100, ww41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(ww40100)), Succ(ww40100)))
new_insertBy044(ww40100, ww41, Succ(ww3120)) → new_insertBy14(ww41)
new_insertBy01(Float(Neg(Zero), Pos(Succ(ww40100))), Float(Neg(Zero), Neg(Succ(Succ(Zero)))), ww41) → new_insertBy057(ww40100, ww41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(ww40100)), Succ(ww40100)))
new_insertBy040(ww40000, ww40100, ww41, Succ(ww2880)) → new_insertBy14(ww41)
new_insertBy053(ww40000, ww40100, :(ww410, ww411), Succ(ww3800)) → new_insertBy01(ww410, Float(Neg(Zero), Neg(Succ(Succ(Zero)))), ww411)
new_insertBy14(:(ww410, ww411)) → new_insertBy01(ww410, Float(Neg(Zero), Neg(Succ(Succ(Zero)))), ww411)
new_insertBy01(Float(Pos(Succ(ww40000)), Pos(Succ(ww40100))), Float(Neg(Zero), Neg(Succ(Succ(Zero)))), ww41) → new_insertBy040(ww40000, ww40100, ww41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(ww40100)), Succ(ww40100)))

The TRS R consists of the following rules:

new_primPlusNat0(Zero, Succ(ww400000)) → Succ(ww400000)
new_primPlusNat0(Succ(ww5500), Succ(ww400000)) → Succ(Succ(new_primPlusNat0(ww5500, ww400000)))
new_primPlusNat0(Zero, Zero) → Zero
new_primPlusNat0(Succ(ww5500), Zero) → Succ(ww5500)

The set Q consists of the following terms:

new_primPlusNat0(Succ(x0), Succ(x1))
new_primPlusNat0(Zero, Zero)
new_primPlusNat0(Zero, Succ(x0))
new_primPlusNat0(Succ(x0), Zero)

We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ CR
    ↳ HASKELL
      ↳ BR
        ↳ HASKELL
          ↳ COR
            ↳ HASKELL
              ↳ Narrow
                ↳ AND
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                    ↳ DependencyGraphProof
                      ↳ AND
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
QDP
                          ↳ QDPSizeChangeProof
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_insertBy01(Float(Neg(Zero), Neg(Succ(ww40100))), Float(Pos(Zero), Pos(Succ(Succ(Succ(ww310000))))), ww41) → new_insertBy028(ww40100, ww310000, ww41, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat1(ww310000, ww40100), Succ(ww40100)), Succ(ww40100)), Succ(ww40100)))
new_insertBy024(ww40000, ww40100, ww310000, ww41, Succ(ww1890)) → new_insertBy8(ww310000, ww41)
new_insertBy015(ww40100, ww310000, ww41, Succ(ww1220)) → new_insertBy8(ww310000, ww41)
new_insertBy01(Float(Pos(Succ(ww40000)), Neg(Succ(ww40100))), Float(Pos(Zero), Pos(Succ(Succ(Succ(ww310000))))), ww41) → new_insertBy011(ww40000, ww40100, ww310000, ww41, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat1(ww310000, ww40100), Succ(ww40100)), Succ(ww40100)), Succ(ww40100)))
new_insertBy01(Float(Neg(Succ(ww40000)), Neg(Succ(ww40100))), Float(Pos(Zero), Pos(Succ(Succ(Succ(ww310000))))), ww41) → new_insertBy024(ww40000, ww40100, ww310000, ww41, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat1(ww310000, ww40100), Succ(ww40100)), Succ(ww40100)), Succ(ww40100)))
new_insertBy8(ww310000, :(ww410, ww411)) → new_insertBy01(ww410, Float(Pos(Zero), Pos(Succ(Succ(Succ(ww310000))))), ww411)
new_insertBy028(ww40100, ww310000, ww41, Succ(ww2130)) → new_insertBy8(ww310000, ww41)
new_insertBy01(Float(Pos(Zero), Neg(Succ(ww40100))), Float(Pos(Zero), Pos(Succ(Succ(Succ(ww310000))))), ww41) → new_insertBy015(ww40100, ww310000, ww41, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat1(ww310000, ww40100), Succ(ww40100)), Succ(ww40100)), Succ(ww40100)))
new_insertBy011(ww40000, ww40100, ww310000, :(ww410, ww411), Succ(ww980)) → new_insertBy01(ww410, Float(Pos(Zero), Pos(Succ(Succ(Succ(ww310000))))), ww411)

The TRS R consists of the following rules:

new_primPlusNat1(Zero, ww40000) → Succ(ww40000)
new_primPlusNat0(Zero, Zero) → Zero
new_primMulNat1(Zero, ww40000) → Zero
new_primPlusNat1(Succ(ww550), ww40000) → Succ(Succ(new_primPlusNat0(ww550, ww40000)))
new_primPlusNat0(Succ(ww5500), Zero) → Succ(ww5500)
new_primPlusNat0(Zero, Succ(ww400000)) → Succ(ww400000)
new_primPlusNat0(Succ(ww5500), Succ(ww400000)) → Succ(Succ(new_primPlusNat0(ww5500, ww400000)))
new_primMulNat1(Succ(ww30000), ww40000) → new_primPlusNat1(new_primMulNat1(ww30000, ww40000), ww40000)

The set Q consists of the following terms:

new_primPlusNat0(Succ(x0), Succ(x1))
new_primPlusNat0(Zero, Zero)
new_primPlusNat0(Zero, Succ(x0))
new_primPlusNat0(Succ(x0), Zero)
new_primPlusNat1(Succ(x0), x1)
new_primMulNat1(Zero, x0)
new_primPlusNat1(Zero, x0)
new_primMulNat1(Succ(x0), x1)

We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ CR
    ↳ HASKELL
      ↳ BR
        ↳ HASKELL
          ↳ COR
            ↳ HASKELL
              ↳ Narrow
                ↳ AND
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                    ↳ DependencyGraphProof
                      ↳ AND
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
QDP
                          ↳ QDPSizeChangeProof
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_insertBy01(Float(Pos(Succ(ww40000)), Pos(Succ(ww40100))), Float(Neg(Zero), Neg(Succ(Succ(Succ(ww310000))))), ww41) → new_insertBy039(ww40000, ww40100, ww310000, ww41, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat1(ww310000, ww40100), Succ(ww40100)), Succ(ww40100)), Succ(ww40100)))
new_insertBy043(ww40100, ww310000, ww41, Succ(ww3080)) → new_insertBy13(ww310000, ww41)
new_insertBy13(ww310000, :(ww410, ww411)) → new_insertBy01(ww410, Float(Neg(Zero), Neg(Succ(Succ(Succ(ww310000))))), ww411)
new_insertBy052(ww40000, ww40100, ww310000, :(ww410, ww411), Succ(ww3760)) → new_insertBy01(ww410, Float(Neg(Zero), Neg(Succ(Succ(Succ(ww310000))))), ww411)
new_insertBy01(Float(Neg(Succ(ww40000)), Pos(Succ(ww40100))), Float(Neg(Zero), Neg(Succ(Succ(Succ(ww310000))))), ww41) → new_insertBy052(ww40000, ww40100, ww310000, ww41, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat1(ww310000, ww40100), Succ(ww40100)), Succ(ww40100)), Succ(ww40100)))
new_insertBy056(ww40100, ww310000, ww41, Succ(ww4000)) → new_insertBy13(ww310000, ww41)
new_insertBy01(Float(Pos(Zero), Pos(Succ(ww40100))), Float(Neg(Zero), Neg(Succ(Succ(Succ(ww310000))))), ww41) → new_insertBy043(ww40100, ww310000, ww41, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat1(ww310000, ww40100), Succ(ww40100)), Succ(ww40100)), Succ(ww40100)))
new_insertBy039(ww40000, ww40100, ww310000, ww41, Succ(ww2840)) → new_insertBy13(ww310000, ww41)
new_insertBy01(Float(Neg(Zero), Pos(Succ(ww40100))), Float(Neg(Zero), Neg(Succ(Succ(Succ(ww310000))))), ww41) → new_insertBy056(ww40100, ww310000, ww41, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat1(ww310000, ww40100), Succ(ww40100)), Succ(ww40100)), Succ(ww40100)))

The TRS R consists of the following rules:

new_primPlusNat1(Zero, ww40000) → Succ(ww40000)
new_primPlusNat0(Zero, Zero) → Zero
new_primMulNat1(Zero, ww40000) → Zero
new_primPlusNat1(Succ(ww550), ww40000) → Succ(Succ(new_primPlusNat0(ww550, ww40000)))
new_primPlusNat0(Succ(ww5500), Zero) → Succ(ww5500)
new_primPlusNat0(Zero, Succ(ww400000)) → Succ(ww400000)
new_primPlusNat0(Succ(ww5500), Succ(ww400000)) → Succ(Succ(new_primPlusNat0(ww5500, ww400000)))
new_primMulNat1(Succ(ww30000), ww40000) → new_primPlusNat1(new_primMulNat1(ww30000, ww40000), ww40000)

The set Q consists of the following terms:

new_primPlusNat0(Succ(x0), Succ(x1))
new_primPlusNat0(Zero, Zero)
new_primPlusNat0(Zero, Succ(x0))
new_primPlusNat0(Succ(x0), Zero)
new_primPlusNat1(Succ(x0), x1)
new_primMulNat1(Zero, x0)
new_primPlusNat1(Zero, x0)
new_primMulNat1(Succ(x0), x1)

We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ CR
    ↳ HASKELL
      ↳ BR
        ↳ HASKELL
          ↳ COR
            ↳ HASKELL
              ↳ Narrow
                ↳ AND
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                    ↳ DependencyGraphProof
                      ↳ AND
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
QDP
                          ↳ QDPSizeChangeProof
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_insertBy030(ww40100, ww310000, ww41, Succ(ww2190)) → new_insertBy9(ww310000, ww41)
new_insertBy013(ww40000, ww40100, ww310000, :(ww410, ww411), Succ(ww1040)) → new_insertBy01(ww410, Float(Pos(Zero), Neg(Succ(Succ(Succ(ww310000))))), ww411)
new_insertBy9(ww310000, :(ww410, ww411)) → new_insertBy01(ww410, Float(Pos(Zero), Neg(Succ(Succ(Succ(ww310000))))), ww411)
new_insertBy01(Float(Neg(Zero), Pos(Succ(ww40100))), Float(Pos(Zero), Neg(Succ(Succ(Succ(ww310000))))), ww41) → new_insertBy030(ww40100, ww310000, ww41, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat1(ww310000, ww40100), Succ(ww40100)), Succ(ww40100)), Succ(ww40100)))
new_insertBy01(Float(Pos(Succ(ww40000)), Pos(Succ(ww40100))), Float(Pos(Zero), Neg(Succ(Succ(Succ(ww310000))))), ww41) → new_insertBy013(ww40000, ww40100, ww310000, ww41, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat1(ww310000, ww40100), Succ(ww40100)), Succ(ww40100)), Succ(ww40100)))
new_insertBy01(Float(Pos(Zero), Pos(Succ(ww40100))), Float(Pos(Zero), Neg(Succ(Succ(Succ(ww310000))))), ww41) → new_insertBy017(ww40100, ww310000, ww41, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat1(ww310000, ww40100), Succ(ww40100)), Succ(ww40100)), Succ(ww40100)))
new_insertBy01(Float(Neg(Succ(ww40000)), Pos(Succ(ww40100))), Float(Pos(Zero), Neg(Succ(Succ(Succ(ww310000))))), ww41) → new_insertBy026(ww40000, ww40100, ww310000, ww41, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat1(ww310000, ww40100), Succ(ww40100)), Succ(ww40100)), Succ(ww40100)))
new_insertBy026(ww40000, ww40100, ww310000, ww41, Succ(ww1950)) → new_insertBy9(ww310000, ww41)
new_insertBy017(ww40100, ww310000, ww41, Succ(ww1280)) → new_insertBy9(ww310000, ww41)

The TRS R consists of the following rules:

new_primPlusNat1(Zero, ww40000) → Succ(ww40000)
new_primPlusNat0(Zero, Zero) → Zero
new_primMulNat1(Zero, ww40000) → Zero
new_primPlusNat1(Succ(ww550), ww40000) → Succ(Succ(new_primPlusNat0(ww550, ww40000)))
new_primPlusNat0(Succ(ww5500), Zero) → Succ(ww5500)
new_primPlusNat0(Zero, Succ(ww400000)) → Succ(ww400000)
new_primPlusNat0(Succ(ww5500), Succ(ww400000)) → Succ(Succ(new_primPlusNat0(ww5500, ww400000)))
new_primMulNat1(Succ(ww30000), ww40000) → new_primPlusNat1(new_primMulNat1(ww30000, ww40000), ww40000)

The set Q consists of the following terms:

new_primPlusNat0(Succ(x0), Succ(x1))
new_primPlusNat0(Zero, Zero)
new_primPlusNat0(Zero, Succ(x0))
new_primPlusNat0(Succ(x0), Zero)
new_primPlusNat1(Succ(x0), x1)
new_primMulNat1(Zero, x0)
new_primPlusNat1(Zero, x0)
new_primMulNat1(Succ(x0), x1)

We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ CR
    ↳ HASKELL
      ↳ BR
        ↳ HASKELL
          ↳ COR
            ↳ HASKELL
              ↳ Narrow
                ↳ AND
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                    ↳ DependencyGraphProof
                      ↳ AND
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
QDP
                          ↳ UsableRulesProof
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_insertBy01(Float(Pos(Zero), Pos(Succ(ww40100))), Float(Pos(Zero), Neg(Succ(Zero))), ww41) → new_insertBy3(ww41)
new_insertBy01(Float(Neg(Succ(ww40000)), Pos(Succ(ww40100))), Float(Pos(Zero), Neg(Succ(Zero))), ww41) → new_insertBy3(ww41)
new_insertBy3(:(ww410, ww411)) → new_insertBy01(ww410, Float(Pos(Zero), Neg(Succ(Zero))), ww411)
new_insertBy01(Float(Neg(Zero), Pos(Succ(ww40100))), Float(Pos(Zero), Neg(Succ(Zero))), ww41) → new_insertBy3(ww41)
new_insertBy01(Float(Pos(Succ(ww40000)), Pos(Succ(ww40100))), Float(Pos(Zero), Neg(Succ(Zero))), :(ww410, ww411)) → new_insertBy01(ww410, Float(Pos(Zero), Neg(Succ(Zero))), ww411)

The TRS R consists of the following rules:

new_primPlusNat1(Zero, ww40000) → Succ(ww40000)
new_primPlusNat0(Zero, Zero) → Zero
new_primMulNat1(Zero, ww40000) → Zero
new_primPlusNat1(Succ(ww550), ww40000) → Succ(Succ(new_primPlusNat0(ww550, ww40000)))
new_primPlusNat0(Succ(ww5500), Zero) → Succ(ww5500)
new_primPlusNat0(Zero, Succ(ww400000)) → Succ(ww400000)
new_primPlusNat0(Succ(ww5500), Succ(ww400000)) → Succ(Succ(new_primPlusNat0(ww5500, ww400000)))
new_primMulNat1(Succ(ww30000), ww40000) → new_primPlusNat1(new_primMulNat1(ww30000, ww40000), ww40000)

The set Q consists of the following terms:

new_primPlusNat0(Succ(x0), Succ(x1))
new_primPlusNat0(Zero, Zero)
new_primPlusNat0(Zero, Succ(x0))
new_primPlusNat0(Succ(x0), Zero)
new_primPlusNat1(Succ(x0), x1)
new_primMulNat1(Zero, x0)
new_primPlusNat1(Zero, x0)
new_primMulNat1(Succ(x0), x1)

We have to consider all minimal (P,Q,R)-chains.
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [15] we can delete all non-usable rules [17] from R.

↳ HASKELL
  ↳ CR
    ↳ HASKELL
      ↳ BR
        ↳ HASKELL
          ↳ COR
            ↳ HASKELL
              ↳ Narrow
                ↳ AND
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                    ↳ DependencyGraphProof
                      ↳ AND
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                          ↳ UsableRulesProof
QDP
                              ↳ QReductionProof
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_insertBy01(Float(Pos(Zero), Pos(Succ(ww40100))), Float(Pos(Zero), Neg(Succ(Zero))), ww41) → new_insertBy3(ww41)
new_insertBy01(Float(Neg(Succ(ww40000)), Pos(Succ(ww40100))), Float(Pos(Zero), Neg(Succ(Zero))), ww41) → new_insertBy3(ww41)
new_insertBy3(:(ww410, ww411)) → new_insertBy01(ww410, Float(Pos(Zero), Neg(Succ(Zero))), ww411)
new_insertBy01(Float(Neg(Zero), Pos(Succ(ww40100))), Float(Pos(Zero), Neg(Succ(Zero))), ww41) → new_insertBy3(ww41)
new_insertBy01(Float(Pos(Succ(ww40000)), Pos(Succ(ww40100))), Float(Pos(Zero), Neg(Succ(Zero))), :(ww410, ww411)) → new_insertBy01(ww410, Float(Pos(Zero), Neg(Succ(Zero))), ww411)

R is empty.
The set Q consists of the following terms:

new_primPlusNat0(Succ(x0), Succ(x1))
new_primPlusNat0(Zero, Zero)
new_primPlusNat0(Zero, Succ(x0))
new_primPlusNat0(Succ(x0), Zero)
new_primPlusNat1(Succ(x0), x1)
new_primMulNat1(Zero, x0)
new_primPlusNat1(Zero, x0)
new_primMulNat1(Succ(x0), x1)

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.

new_primPlusNat0(Succ(x0), Succ(x1))
new_primPlusNat0(Zero, Zero)
new_primPlusNat0(Zero, Succ(x0))
new_primPlusNat0(Succ(x0), Zero)
new_primPlusNat1(Succ(x0), x1)
new_primMulNat1(Zero, x0)
new_primPlusNat1(Zero, x0)
new_primMulNat1(Succ(x0), x1)



↳ HASKELL
  ↳ CR
    ↳ HASKELL
      ↳ BR
        ↳ HASKELL
          ↳ COR
            ↳ HASKELL
              ↳ Narrow
                ↳ AND
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                    ↳ DependencyGraphProof
                      ↳ AND
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                          ↳ UsableRulesProof
                            ↳ QDP
                              ↳ QReductionProof
QDP
                                  ↳ QDPSizeChangeProof
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_insertBy01(Float(Pos(Zero), Pos(Succ(ww40100))), Float(Pos(Zero), Neg(Succ(Zero))), ww41) → new_insertBy3(ww41)
new_insertBy01(Float(Neg(Succ(ww40000)), Pos(Succ(ww40100))), Float(Pos(Zero), Neg(Succ(Zero))), ww41) → new_insertBy3(ww41)
new_insertBy3(:(ww410, ww411)) → new_insertBy01(ww410, Float(Pos(Zero), Neg(Succ(Zero))), ww411)
new_insertBy01(Float(Pos(Succ(ww40000)), Pos(Succ(ww40100))), Float(Pos(Zero), Neg(Succ(Zero))), :(ww410, ww411)) → new_insertBy01(ww410, Float(Pos(Zero), Neg(Succ(Zero))), ww411)
new_insertBy01(Float(Neg(Zero), Pos(Succ(ww40100))), Float(Pos(Zero), Neg(Succ(Zero))), ww41) → new_insertBy3(ww41)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ CR
    ↳ HASKELL
      ↳ BR
        ↳ HASKELL
          ↳ COR
            ↳ HASKELL
              ↳ Narrow
                ↳ AND
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                    ↳ DependencyGraphProof
                      ↳ AND
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
QDP
                          ↳ UsableRulesProof
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_insertBy038(ww40000, ww40100, ww41, Succ(ww2820)) → new_insertBy12(ww41)
new_insertBy01(Float(Neg(Zero), Neg(Succ(ww40100))), Float(Neg(Zero), Pos(Succ(Succ(Zero)))), ww41) → new_insertBy055(ww40100, ww41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(ww40100)), Succ(ww40100)))
new_insertBy12(:(ww410, ww411)) → new_insertBy01(ww410, Float(Neg(Zero), Pos(Succ(Succ(Zero)))), ww411)
new_insertBy042(ww40100, ww41, Succ(ww3060)) → new_insertBy12(ww41)
new_insertBy01(Float(Pos(Zero), Neg(Succ(ww40100))), Float(Neg(Zero), Pos(Succ(Succ(Zero)))), ww41) → new_insertBy042(ww40100, ww41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(ww40100)), Succ(ww40100)))
new_insertBy01(Float(Pos(Succ(ww40000)), Neg(Succ(ww40100))), Float(Neg(Zero), Pos(Succ(Succ(Zero)))), ww41) → new_insertBy038(ww40000, ww40100, ww41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(ww40100)), Succ(ww40100)))
new_insertBy055(ww40100, ww41, Succ(ww3980)) → new_insertBy12(ww41)
new_insertBy051(ww40000, ww40100, :(ww410, ww411), Succ(ww3740)) → new_insertBy01(ww410, Float(Neg(Zero), Pos(Succ(Succ(Zero)))), ww411)
new_insertBy01(Float(Neg(Succ(ww40000)), Neg(Succ(ww40100))), Float(Neg(Zero), Pos(Succ(Succ(Zero)))), ww41) → new_insertBy051(ww40000, ww40100, ww41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(ww40100)), Succ(ww40100)))

The TRS R consists of the following rules:

new_primPlusNat1(Zero, ww40000) → Succ(ww40000)
new_primPlusNat0(Zero, Zero) → Zero
new_primMulNat1(Zero, ww40000) → Zero
new_primPlusNat1(Succ(ww550), ww40000) → Succ(Succ(new_primPlusNat0(ww550, ww40000)))
new_primPlusNat0(Succ(ww5500), Zero) → Succ(ww5500)
new_primPlusNat0(Zero, Succ(ww400000)) → Succ(ww400000)
new_primPlusNat0(Succ(ww5500), Succ(ww400000)) → Succ(Succ(new_primPlusNat0(ww5500, ww400000)))
new_primMulNat1(Succ(ww30000), ww40000) → new_primPlusNat1(new_primMulNat1(ww30000, ww40000), ww40000)

The set Q consists of the following terms:

new_primPlusNat0(Succ(x0), Succ(x1))
new_primPlusNat0(Zero, Zero)
new_primPlusNat0(Zero, Succ(x0))
new_primPlusNat0(Succ(x0), Zero)
new_primPlusNat1(Succ(x0), x1)
new_primMulNat1(Zero, x0)
new_primPlusNat1(Zero, x0)
new_primMulNat1(Succ(x0), x1)

We have to consider all minimal (P,Q,R)-chains.
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [15] we can delete all non-usable rules [17] from R.

↳ HASKELL
  ↳ CR
    ↳ HASKELL
      ↳ BR
        ↳ HASKELL
          ↳ COR
            ↳ HASKELL
              ↳ Narrow
                ↳ AND
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                    ↳ DependencyGraphProof
                      ↳ AND
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                          ↳ UsableRulesProof
QDP
                              ↳ QReductionProof
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_insertBy038(ww40000, ww40100, ww41, Succ(ww2820)) → new_insertBy12(ww41)
new_insertBy01(Float(Neg(Zero), Neg(Succ(ww40100))), Float(Neg(Zero), Pos(Succ(Succ(Zero)))), ww41) → new_insertBy055(ww40100, ww41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(ww40100)), Succ(ww40100)))
new_insertBy12(:(ww410, ww411)) → new_insertBy01(ww410, Float(Neg(Zero), Pos(Succ(Succ(Zero)))), ww411)
new_insertBy042(ww40100, ww41, Succ(ww3060)) → new_insertBy12(ww41)
new_insertBy01(Float(Pos(Zero), Neg(Succ(ww40100))), Float(Neg(Zero), Pos(Succ(Succ(Zero)))), ww41) → new_insertBy042(ww40100, ww41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(ww40100)), Succ(ww40100)))
new_insertBy01(Float(Pos(Succ(ww40000)), Neg(Succ(ww40100))), Float(Neg(Zero), Pos(Succ(Succ(Zero)))), ww41) → new_insertBy038(ww40000, ww40100, ww41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(ww40100)), Succ(ww40100)))
new_insertBy055(ww40100, ww41, Succ(ww3980)) → new_insertBy12(ww41)
new_insertBy051(ww40000, ww40100, :(ww410, ww411), Succ(ww3740)) → new_insertBy01(ww410, Float(Neg(Zero), Pos(Succ(Succ(Zero)))), ww411)
new_insertBy01(Float(Neg(Succ(ww40000)), Neg(Succ(ww40100))), Float(Neg(Zero), Pos(Succ(Succ(Zero)))), ww41) → new_insertBy051(ww40000, ww40100, ww41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(ww40100)), Succ(ww40100)))

The TRS R consists of the following rules:

new_primPlusNat0(Zero, Succ(ww400000)) → Succ(ww400000)
new_primPlusNat0(Succ(ww5500), Succ(ww400000)) → Succ(Succ(new_primPlusNat0(ww5500, ww400000)))
new_primPlusNat0(Zero, Zero) → Zero
new_primPlusNat0(Succ(ww5500), Zero) → Succ(ww5500)

The set Q consists of the following terms:

new_primPlusNat0(Succ(x0), Succ(x1))
new_primPlusNat0(Zero, Zero)
new_primPlusNat0(Zero, Succ(x0))
new_primPlusNat0(Succ(x0), Zero)
new_primPlusNat1(Succ(x0), x1)
new_primMulNat1(Zero, x0)
new_primPlusNat1(Zero, x0)
new_primMulNat1(Succ(x0), x1)

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.

new_primPlusNat1(Succ(x0), x1)
new_primMulNat1(Zero, x0)
new_primPlusNat1(Zero, x0)
new_primMulNat1(Succ(x0), x1)



↳ HASKELL
  ↳ CR
    ↳ HASKELL
      ↳ BR
        ↳ HASKELL
          ↳ COR
            ↳ HASKELL
              ↳ Narrow
                ↳ AND
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                    ↳ DependencyGraphProof
                      ↳ AND
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                          ↳ UsableRulesProof
                            ↳ QDP
                              ↳ QReductionProof
QDP
                                  ↳ QDPSizeChangeProof
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_insertBy038(ww40000, ww40100, ww41, Succ(ww2820)) → new_insertBy12(ww41)
new_insertBy01(Float(Neg(Zero), Neg(Succ(ww40100))), Float(Neg(Zero), Pos(Succ(Succ(Zero)))), ww41) → new_insertBy055(ww40100, ww41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(ww40100)), Succ(ww40100)))
new_insertBy12(:(ww410, ww411)) → new_insertBy01(ww410, Float(Neg(Zero), Pos(Succ(Succ(Zero)))), ww411)
new_insertBy01(Float(Pos(Zero), Neg(Succ(ww40100))), Float(Neg(Zero), Pos(Succ(Succ(Zero)))), ww41) → new_insertBy042(ww40100, ww41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(ww40100)), Succ(ww40100)))
new_insertBy042(ww40100, ww41, Succ(ww3060)) → new_insertBy12(ww41)
new_insertBy01(Float(Pos(Succ(ww40000)), Neg(Succ(ww40100))), Float(Neg(Zero), Pos(Succ(Succ(Zero)))), ww41) → new_insertBy038(ww40000, ww40100, ww41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(ww40100)), Succ(ww40100)))
new_insertBy055(ww40100, ww41, Succ(ww3980)) → new_insertBy12(ww41)
new_insertBy01(Float(Neg(Succ(ww40000)), Neg(Succ(ww40100))), Float(Neg(Zero), Pos(Succ(Succ(Zero)))), ww41) → new_insertBy051(ww40000, ww40100, ww41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(ww40100)), Succ(ww40100)))
new_insertBy051(ww40000, ww40100, :(ww410, ww411), Succ(ww3740)) → new_insertBy01(ww410, Float(Neg(Zero), Pos(Succ(Succ(Zero)))), ww411)

The TRS R consists of the following rules:

new_primPlusNat0(Zero, Succ(ww400000)) → Succ(ww400000)
new_primPlusNat0(Succ(ww5500), Succ(ww400000)) → Succ(Succ(new_primPlusNat0(ww5500, ww400000)))
new_primPlusNat0(Zero, Zero) → Zero
new_primPlusNat0(Succ(ww5500), Zero) → Succ(ww5500)

The set Q consists of the following terms:

new_primPlusNat0(Succ(x0), Succ(x1))
new_primPlusNat0(Zero, Zero)
new_primPlusNat0(Zero, Succ(x0))
new_primPlusNat0(Succ(x0), Zero)

We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ CR
    ↳ HASKELL
      ↳ BR
        ↳ HASKELL
          ↳ COR
            ↳ HASKELL
              ↳ Narrow
                ↳ AND
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                    ↳ DependencyGraphProof
                      ↳ AND
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
QDP
                          ↳ UsableRulesProof
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_insertBy027(ww40000, ww40100, ww41, Succ(ww1990)) → new_insertBy10(ww41)
new_insertBy10(:(ww410, ww411)) → new_insertBy01(ww410, Float(Pos(Zero), Neg(Succ(Succ(Zero)))), ww411)
new_insertBy01(Float(Pos(Succ(ww40000)), Pos(Succ(ww40100))), Float(Pos(Zero), Neg(Succ(Succ(Zero)))), ww41) → new_insertBy014(ww40000, ww40100, ww41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(ww40100)), Succ(ww40100)))
new_insertBy01(Float(Neg(Zero), Pos(Succ(ww40100))), Float(Pos(Zero), Neg(Succ(Succ(Zero)))), ww41) → new_insertBy031(ww40100, ww41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(ww40100)), Succ(ww40100)))
new_insertBy014(ww40000, ww40100, :(ww410, ww411), Succ(ww1080)) → new_insertBy01(ww410, Float(Pos(Zero), Neg(Succ(Succ(Zero)))), ww411)
new_insertBy031(ww40100, ww41, Succ(ww2230)) → new_insertBy10(ww41)
new_insertBy01(Float(Pos(Zero), Pos(Succ(ww40100))), Float(Pos(Zero), Neg(Succ(Succ(Zero)))), ww41) → new_insertBy018(ww40100, ww41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(ww40100)), Succ(ww40100)))
new_insertBy018(ww40100, ww41, Succ(ww1320)) → new_insertBy10(ww41)
new_insertBy01(Float(Neg(Succ(ww40000)), Pos(Succ(ww40100))), Float(Pos(Zero), Neg(Succ(Succ(Zero)))), ww41) → new_insertBy027(ww40000, ww40100, ww41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(ww40100)), Succ(ww40100)))

The TRS R consists of the following rules:

new_primPlusNat1(Zero, ww40000) → Succ(ww40000)
new_primPlusNat0(Zero, Zero) → Zero
new_primMulNat1(Zero, ww40000) → Zero
new_primPlusNat1(Succ(ww550), ww40000) → Succ(Succ(new_primPlusNat0(ww550, ww40000)))
new_primPlusNat0(Succ(ww5500), Zero) → Succ(ww5500)
new_primPlusNat0(Zero, Succ(ww400000)) → Succ(ww400000)
new_primPlusNat0(Succ(ww5500), Succ(ww400000)) → Succ(Succ(new_primPlusNat0(ww5500, ww400000)))
new_primMulNat1(Succ(ww30000), ww40000) → new_primPlusNat1(new_primMulNat1(ww30000, ww40000), ww40000)

The set Q consists of the following terms:

new_primPlusNat0(Succ(x0), Succ(x1))
new_primPlusNat0(Zero, Zero)
new_primPlusNat0(Zero, Succ(x0))
new_primPlusNat0(Succ(x0), Zero)
new_primPlusNat1(Succ(x0), x1)
new_primMulNat1(Zero, x0)
new_primPlusNat1(Zero, x0)
new_primMulNat1(Succ(x0), x1)

We have to consider all minimal (P,Q,R)-chains.
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [15] we can delete all non-usable rules [17] from R.

↳ HASKELL
  ↳ CR
    ↳ HASKELL
      ↳ BR
        ↳ HASKELL
          ↳ COR
            ↳ HASKELL
              ↳ Narrow
                ↳ AND
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                    ↳ DependencyGraphProof
                      ↳ AND
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                          ↳ UsableRulesProof
QDP
                              ↳ QReductionProof
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_insertBy027(ww40000, ww40100, ww41, Succ(ww1990)) → new_insertBy10(ww41)
new_insertBy10(:(ww410, ww411)) → new_insertBy01(ww410, Float(Pos(Zero), Neg(Succ(Succ(Zero)))), ww411)
new_insertBy01(Float(Pos(Succ(ww40000)), Pos(Succ(ww40100))), Float(Pos(Zero), Neg(Succ(Succ(Zero)))), ww41) → new_insertBy014(ww40000, ww40100, ww41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(ww40100)), Succ(ww40100)))
new_insertBy01(Float(Neg(Zero), Pos(Succ(ww40100))), Float(Pos(Zero), Neg(Succ(Succ(Zero)))), ww41) → new_insertBy031(ww40100, ww41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(ww40100)), Succ(ww40100)))
new_insertBy014(ww40000, ww40100, :(ww410, ww411), Succ(ww1080)) → new_insertBy01(ww410, Float(Pos(Zero), Neg(Succ(Succ(Zero)))), ww411)
new_insertBy031(ww40100, ww41, Succ(ww2230)) → new_insertBy10(ww41)
new_insertBy01(Float(Pos(Zero), Pos(Succ(ww40100))), Float(Pos(Zero), Neg(Succ(Succ(Zero)))), ww41) → new_insertBy018(ww40100, ww41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(ww40100)), Succ(ww40100)))
new_insertBy018(ww40100, ww41, Succ(ww1320)) → new_insertBy10(ww41)
new_insertBy01(Float(Neg(Succ(ww40000)), Pos(Succ(ww40100))), Float(Pos(Zero), Neg(Succ(Succ(Zero)))), ww41) → new_insertBy027(ww40000, ww40100, ww41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(ww40100)), Succ(ww40100)))

The TRS R consists of the following rules:

new_primPlusNat0(Zero, Succ(ww400000)) → Succ(ww400000)
new_primPlusNat0(Succ(ww5500), Succ(ww400000)) → Succ(Succ(new_primPlusNat0(ww5500, ww400000)))
new_primPlusNat0(Zero, Zero) → Zero
new_primPlusNat0(Succ(ww5500), Zero) → Succ(ww5500)

The set Q consists of the following terms:

new_primPlusNat0(Succ(x0), Succ(x1))
new_primPlusNat0(Zero, Zero)
new_primPlusNat0(Zero, Succ(x0))
new_primPlusNat0(Succ(x0), Zero)
new_primPlusNat1(Succ(x0), x1)
new_primMulNat1(Zero, x0)
new_primPlusNat1(Zero, x0)
new_primMulNat1(Succ(x0), x1)

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.

new_primPlusNat1(Succ(x0), x1)
new_primMulNat1(Zero, x0)
new_primPlusNat1(Zero, x0)
new_primMulNat1(Succ(x0), x1)



↳ HASKELL
  ↳ CR
    ↳ HASKELL
      ↳ BR
        ↳ HASKELL
          ↳ COR
            ↳ HASKELL
              ↳ Narrow
                ↳ AND
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                    ↳ DependencyGraphProof
                      ↳ AND
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                          ↳ UsableRulesProof
                            ↳ QDP
                              ↳ QReductionProof
QDP
                                  ↳ QDPSizeChangeProof
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_insertBy027(ww40000, ww40100, ww41, Succ(ww1990)) → new_insertBy10(ww41)
new_insertBy10(:(ww410, ww411)) → new_insertBy01(ww410, Float(Pos(Zero), Neg(Succ(Succ(Zero)))), ww411)
new_insertBy01(Float(Neg(Zero), Pos(Succ(ww40100))), Float(Pos(Zero), Neg(Succ(Succ(Zero)))), ww41) → new_insertBy031(ww40100, ww41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(ww40100)), Succ(ww40100)))
new_insertBy01(Float(Pos(Succ(ww40000)), Pos(Succ(ww40100))), Float(Pos(Zero), Neg(Succ(Succ(Zero)))), ww41) → new_insertBy014(ww40000, ww40100, ww41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(ww40100)), Succ(ww40100)))
new_insertBy014(ww40000, ww40100, :(ww410, ww411), Succ(ww1080)) → new_insertBy01(ww410, Float(Pos(Zero), Neg(Succ(Succ(Zero)))), ww411)
new_insertBy031(ww40100, ww41, Succ(ww2230)) → new_insertBy10(ww41)
new_insertBy01(Float(Pos(Zero), Pos(Succ(ww40100))), Float(Pos(Zero), Neg(Succ(Succ(Zero)))), ww41) → new_insertBy018(ww40100, ww41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(ww40100)), Succ(ww40100)))
new_insertBy018(ww40100, ww41, Succ(ww1320)) → new_insertBy10(ww41)
new_insertBy01(Float(Neg(Succ(ww40000)), Pos(Succ(ww40100))), Float(Pos(Zero), Neg(Succ(Succ(Zero)))), ww41) → new_insertBy027(ww40000, ww40100, ww41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(ww40100)), Succ(ww40100)))

The TRS R consists of the following rules:

new_primPlusNat0(Zero, Succ(ww400000)) → Succ(ww400000)
new_primPlusNat0(Succ(ww5500), Succ(ww400000)) → Succ(Succ(new_primPlusNat0(ww5500, ww400000)))
new_primPlusNat0(Zero, Zero) → Zero
new_primPlusNat0(Succ(ww5500), Zero) → Succ(ww5500)

The set Q consists of the following terms:

new_primPlusNat0(Succ(x0), Succ(x1))
new_primPlusNat0(Zero, Zero)
new_primPlusNat0(Zero, Succ(x0))
new_primPlusNat0(Succ(x0), Zero)

We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ CR
    ↳ HASKELL
      ↳ BR
        ↳ HASKELL
          ↳ COR
            ↳ HASKELL
              ↳ Narrow
                ↳ AND
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                    ↳ DependencyGraphProof
                      ↳ AND
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
QDP
                          ↳ QDPSizeChangeProof
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_insertBy068(ww38, ww3900, ww40, ww4100, ww42, Succ(Succ(ww27000)), Zero) → new_insertBy074(ww38, ww3900, ww40, ww4100, ww42)
new_insertBy045(ww44, Neg(Succ(ww4500)), ww46, Neg(Succ(ww4700)), ww48, Succ(ww3200)) → new_insertBy076(ww44, ww4500, ww46, ww4700, ww48, ww3200, new_primPlusNat0(new_primMulNat1(ww4700, ww4500), Succ(ww4500)))
new_insertBy032(ww38, Pos(Succ(ww3900)), ww40, Neg(Succ(ww4100)), ww42, Zero) → new_insertBy070(ww38, ww3900, ww40, ww4100, ww42, new_primPlusNat0(new_primMulNat1(ww4100, ww3900), Succ(ww3900)))
new_insertBy01(Float(Pos(Zero), Neg(Succ(ww40100))), Float(Neg(Succ(ww3000)), Pos(Succ(Succ(Succ(ww310000))))), ww41) → new_insertBy033(ww40100, ww3000, ww310000, ww41, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat1(ww310000, ww40100), Succ(ww40100)), Succ(ww40100)), Succ(ww40100)))
new_insertBy01(Float(Neg(Zero), Neg(Succ(ww40100))), Float(Neg(Succ(ww3000)), Pos(Succ(Succ(Zero)))), ww41) → new_insertBy047(ww40100, ww3000, ww41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(ww40100)), Succ(ww40100)))
new_insertBy079(ww44, ww4500, ww46, ww4700, ww48, Succ(ww32000), Zero) → new_insertBy080(ww44, ww4500, ww46, ww4700, ww48)
new_insertBy01(Float(Neg(Zero), Pos(Succ(ww40100))), Float(Neg(Succ(ww3000)), Neg(Succ(Succ(Zero)))), ww41) → new_insertBy049(ww40100, ww3000, ww41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(ww40100)), Succ(ww40100)))
new_insertBy045(ww44, Pos(Zero), ww46, Pos(Succ(ww4700)), ww48, Succ(ww3200)) → new_insertBy4(ww46, Succ(ww4700), ww48)
new_insertBy045(ww44, Neg(Succ(ww4500)), ww46, Neg(Zero), ww48, Succ(ww3200)) → new_insertBy5(ww46, Zero, ww48)
new_insertBy075(ww44, ww4500, ww46, ww4700, ww48, Succ(ww32000), Succ(Zero)) → new_insertBy080(ww44, ww4500, ww46, ww4700, ww48)
new_insertBy071(ww38, ww3900, ww40, ww4100, ww42, Succ(ww26800), Zero) → new_insertBy072(ww38, ww3900, ww40, ww4100, ww42)
new_insertBy072(ww38, ww3900, ww40, ww4100, ww42) → new_insertBy4(ww40, Succ(ww4100), ww42)
new_insertBy01(Float(Neg(Zero), Neg(Succ(ww40100))), Float(Neg(Succ(ww3000)), Pos(Succ(Zero))), ww41) → new_insertBy4(ww3000, Succ(Zero), ww41)
new_insertBy4(ww46, ww470, :(ww480, ww481)) → new_insertBy01(ww480, Float(Neg(Succ(ww46)), Pos(ww470)), ww481)
new_insertBy070(ww38, ww3900, ww40, ww4100, ww42, Succ(ww2640)) → new_insertBy5(ww40, Succ(ww4100), ww42)
new_insertBy045(ww44, Neg(Zero), ww46, Neg(Succ(ww4700)), ww48, Succ(ww3200)) → new_insertBy5(ww46, Succ(ww4700), ww48)
new_insertBy01(Float(Pos(Zero), Pos(Succ(ww40100))), Float(Neg(Succ(ww3000)), Neg(Succ(Zero))), ww41) → new_insertBy5(ww3000, Succ(Zero), ww41)
new_insertBy045(ww44, Neg(Zero), ww46, Neg(Zero), ww48, Succ(ww3200)) → new_insertBy5(ww46, Zero, ww48)
new_insertBy033(ww40100, ww3000, ww310000, ww41, Succ(ww2420)) → new_insertBy4(ww3000, Succ(Succ(Succ(ww310000))), ww41)
new_insertBy084(ww44, ww4500, ww46, ww4700, ww48) → new_insertBy5(ww46, Succ(ww4700), ww48)
new_insertBy046(ww40100, ww3000, ww310000, ww41, Succ(ww3330)) → new_insertBy4(ww3000, Succ(Succ(Succ(ww310000))), ww41)
new_insertBy083(ww44, ww4500, ww46, ww4700, ww48, Succ(ww32000), Zero) → new_insertBy084(ww44, ww4500, ww46, ww4700, ww48)
new_insertBy032(ww38, Neg(Succ(ww3900)), ww40, Pos(Succ(ww4100)), ww42, Zero) → new_insertBy069(ww38, ww3900, ww40, ww4100, ww42, new_primPlusNat0(new_primMulNat1(ww4100, ww3900), Succ(ww3900)))
new_insertBy034(ww40100, ww3000, ww41, Succ(ww2460)) → new_insertBy4(ww3000, Succ(Succ(Zero)), ww41)
new_insertBy079(ww44, ww4500, ww46, ww4700, ww48, Succ(ww32000), Succ(ww35900)) → new_insertBy079(ww44, ww4500, ww46, ww4700, ww48, ww32000, ww35900)
new_insertBy01(Float(Neg(Zero), Neg(Succ(ww40100))), Float(Neg(Succ(ww3000)), Pos(Succ(Succ(Succ(ww310000))))), ww41) → new_insertBy046(ww40100, ww3000, ww310000, ww41, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat1(ww310000, ww40100), Succ(ww40100)), Succ(ww40100)), Succ(ww40100)))
new_insertBy083(ww44, ww4500, ww46, ww4700, ww48, Succ(ww32000), Succ(ww36100)) → new_insertBy083(ww44, ww4500, ww46, ww4700, ww48, ww32000, ww36100)
new_insertBy01(Float(Pos(Zero), Pos(Succ(ww40100))), Float(Neg(Succ(ww3000)), Neg(Succ(Succ(Zero)))), ww41) → new_insertBy036(ww40100, ww3000, ww41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(ww40100)), Succ(ww40100)))
new_insertBy01(Float(Pos(Zero), Pos(Succ(ww40100))), Float(Neg(Succ(ww3000)), Neg(Succ(Succ(Succ(ww310000))))), ww41) → new_insertBy035(ww40100, ww3000, ww310000, ww41, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat1(ww310000, ww40100), Succ(ww40100)), Succ(ww40100)), Succ(ww40100)))
new_insertBy068(ww38, ww3900, ww40, ww4100, ww42, Succ(Succ(ww27000)), Succ(ww23100)) → new_insertBy073(ww38, ww3900, ww40, ww4100, ww42, ww27000, ww23100)
new_insertBy01(Float(Neg(Zero), Pos(Succ(ww40100))), Float(Neg(Succ(ww3000)), Neg(Succ(Zero))), ww41) → new_insertBy5(ww3000, Succ(Zero), ww41)
new_insertBy069(ww38, ww3900, ww40, ww4100, ww42, Succ(ww2620)) → new_insertBy4(ww40, Succ(ww4100), ww42)
new_insertBy01(Float(Pos(Succ(ww40000)), ww401), Float(Neg(Succ(ww3000)), ww31), ww41) → new_insertBy032(ww40000, ww401, ww3000, ww31, ww41, new_primPlusNat0(new_primMulNat1(ww3000, ww40000), Succ(ww40000)))
new_insertBy078(ww44, ww4500, ww46, ww4700, ww48, Succ(ww3550)) → new_insertBy082(ww44, Succ(ww4500), ww46, Succ(ww4700), ww48)
new_insertBy5(ww46, ww470, :(ww480, ww481)) → new_insertBy01(ww480, Float(Neg(Succ(ww46)), Neg(ww470)), ww481)
new_insertBy075(ww44, ww4500, ww46, ww4700, ww48, Succ(ww32000), Succ(Succ(ww35900))) → new_insertBy079(ww44, ww4500, ww46, ww4700, ww48, ww32000, ww35900)
new_insertBy071(ww38, ww3900, ww40, ww4100, ww42, Succ(ww26800), Succ(ww23100)) → new_insertBy071(ww38, ww3900, ww40, ww4100, ww42, ww26800, ww23100)
new_insertBy045(ww44, Pos(Succ(ww4500)), ww46, Pos(Zero), ww48, Succ(ww3200)) → new_insertBy4(ww46, Zero, ww48)
new_insertBy032(ww38, Pos(Succ(ww3900)), ww40, Neg(Succ(ww4100)), ww42, Succ(ww2310)) → new_insertBy068(ww38, ww3900, ww40, ww4100, ww42, new_primPlusNat0(new_primMulNat1(ww4100, ww3900), Succ(ww3900)), ww2310)
new_insertBy036(ww40100, ww3000, ww41, Succ(ww2520)) → new_insertBy5(ww3000, Succ(Succ(Zero)), ww41)
new_insertBy032(ww38, Neg(Succ(ww3900)), ww40, Pos(Succ(ww4100)), ww42, Succ(ww2310)) → new_insertBy067(ww38, ww3900, ww40, ww4100, ww42, new_primPlusNat0(new_primMulNat1(ww4100, ww3900), Succ(ww3900)), ww2310)
new_insertBy049(ww40100, ww3000, ww41, Succ(ww3430)) → new_insertBy5(ww3000, Succ(Succ(Zero)), ww41)
new_insertBy01(Float(Pos(Zero), Neg(Succ(ww40100))), Float(Neg(Succ(ww3000)), Pos(Succ(Zero))), ww41) → new_insertBy4(ww3000, Succ(Zero), ww41)
new_insertBy045(ww44, Pos(ww450), ww46, Neg(ww470), :(ww480, ww481), Succ(ww3200)) → new_insertBy01(ww480, Float(Neg(Succ(ww46)), Neg(ww470)), ww481)
new_insertBy048(ww40100, ww3000, ww310000, ww41, Succ(ww3390)) → new_insertBy5(ww3000, Succ(Succ(Succ(ww310000))), ww41)
new_insertBy01(Float(Pos(Zero), Neg(Succ(ww40100))), Float(Neg(Succ(ww3000)), Pos(Succ(Succ(Zero)))), ww41) → new_insertBy034(ww40100, ww3000, ww41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(ww40100)), Succ(ww40100)))
new_insertBy076(ww44, ww4500, ww46, ww4700, ww48, Succ(ww32000), Succ(Succ(ww36100))) → new_insertBy083(ww44, ww4500, ww46, ww4700, ww48, ww32000, ww36100)
new_insertBy01(Float(Neg(Succ(ww40000)), ww401), Float(Neg(Succ(ww3000)), ww31), ww41) → new_insertBy045(ww40000, ww401, ww3000, ww31, ww41, new_primPlusNat0(new_primMulNat1(ww3000, ww40000), Succ(ww40000)))
new_insertBy081(ww44, ww450, ww46, ww470, :(ww480, ww481)) → new_insertBy01(ww480, Float(Neg(Succ(ww46)), Pos(ww470)), ww481)
new_insertBy01(Float(Neg(Zero), Pos(Succ(ww40100))), Float(Neg(Succ(ww3000)), Neg(Succ(Succ(Succ(ww310000))))), ww41) → new_insertBy048(ww40100, ww3000, ww310000, ww41, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat1(ww310000, ww40100), Succ(ww40100)), Succ(ww40100)), Succ(ww40100)))
new_insertBy075(ww44, ww4500, ww46, ww4700, ww48, ww3200, Zero) → new_insertBy4(ww46, Succ(ww4700), ww48)
new_insertBy077(ww44, ww4500, ww46, ww4700, ww48, Succ(ww3530)) → new_insertBy081(ww44, Succ(ww4500), ww46, Succ(ww4700), ww48)
new_insertBy082(ww44, ww450, ww46, ww470, :(ww480, ww481)) → new_insertBy01(ww480, Float(Neg(Succ(ww46)), Neg(ww470)), ww481)
new_insertBy047(ww40100, ww3000, ww41, Succ(ww3370)) → new_insertBy4(ww3000, Succ(Succ(Zero)), ww41)
new_insertBy073(ww38, ww3900, ww40, ww4100, ww42, Succ(ww27000), Succ(ww23100)) → new_insertBy073(ww38, ww3900, ww40, ww4100, ww42, ww27000, ww23100)
new_insertBy045(ww44, Pos(Succ(ww4500)), ww46, Neg(Succ(ww4700)), ww48, Zero) → new_insertBy078(ww44, ww4500, ww46, ww4700, ww48, new_primPlusNat0(new_primMulNat1(ww4700, ww4500), Succ(ww4500)))
new_insertBy067(ww38, ww3900, ww40, ww4100, ww42, Succ(Succ(ww26800)), Succ(ww23100)) → new_insertBy071(ww38, ww3900, ww40, ww4100, ww42, ww26800, ww23100)
new_insertBy045(ww44, Neg(ww450), ww46, Pos(ww470), :(ww480, ww481), Succ(ww3200)) → new_insertBy01(ww480, Float(Neg(Succ(ww46)), Pos(ww470)), ww481)
new_insertBy073(ww38, ww3900, ww40, ww4100, ww42, Succ(ww27000), Zero) → new_insertBy074(ww38, ww3900, ww40, ww4100, ww42)
new_insertBy067(ww38, ww3900, ww40, ww4100, ww42, Succ(Succ(ww26800)), Zero) → new_insertBy072(ww38, ww3900, ww40, ww4100, ww42)
new_insertBy045(ww44, Pos(Zero), ww46, Pos(Zero), ww48, Succ(ww3200)) → new_insertBy4(ww46, Zero, ww48)
new_insertBy080(ww44, ww4500, ww46, ww4700, ww48) → new_insertBy4(ww46, Succ(ww4700), ww48)
new_insertBy045(ww44, Pos(Succ(ww4500)), ww46, Pos(Succ(ww4700)), ww48, Succ(ww3200)) → new_insertBy075(ww44, ww4500, ww46, ww4700, ww48, ww3200, new_primPlusNat0(new_primMulNat1(ww4700, ww4500), Succ(ww4500)))
new_insertBy045(ww44, Neg(Succ(ww4500)), ww46, Pos(Succ(ww4700)), ww48, Zero) → new_insertBy077(ww44, ww4500, ww46, ww4700, ww48, new_primPlusNat0(new_primMulNat1(ww4700, ww4500), Succ(ww4500)))
new_insertBy074(ww38, ww3900, ww40, ww4100, ww42) → new_insertBy5(ww40, Succ(ww4100), ww42)
new_insertBy035(ww40100, ww3000, ww310000, ww41, Succ(ww2480)) → new_insertBy5(ww3000, Succ(Succ(Succ(ww310000))), ww41)
new_insertBy076(ww44, ww4500, ww46, ww4700, ww48, Succ(ww32000), Succ(Zero)) → new_insertBy084(ww44, ww4500, ww46, ww4700, ww48)
new_insertBy076(ww44, ww4500, ww46, ww4700, ww48, ww3200, Zero) → new_insertBy5(ww46, Succ(ww4700), ww48)

The TRS R consists of the following rules:

new_primPlusNat1(Zero, ww40000) → Succ(ww40000)
new_primPlusNat0(Zero, Zero) → Zero
new_primMulNat1(Zero, ww40000) → Zero
new_primPlusNat1(Succ(ww550), ww40000) → Succ(Succ(new_primPlusNat0(ww550, ww40000)))
new_primPlusNat0(Succ(ww5500), Zero) → Succ(ww5500)
new_primPlusNat0(Zero, Succ(ww400000)) → Succ(ww400000)
new_primPlusNat0(Succ(ww5500), Succ(ww400000)) → Succ(Succ(new_primPlusNat0(ww5500, ww400000)))
new_primMulNat1(Succ(ww30000), ww40000) → new_primPlusNat1(new_primMulNat1(ww30000, ww40000), ww40000)

The set Q consists of the following terms:

new_primPlusNat0(Succ(x0), Succ(x1))
new_primPlusNat0(Zero, Zero)
new_primPlusNat0(Zero, Succ(x0))
new_primPlusNat0(Succ(x0), Zero)
new_primPlusNat1(Succ(x0), x1)
new_primMulNat1(Zero, x0)
new_primPlusNat1(Zero, x0)
new_primMulNat1(Succ(x0), x1)

We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ CR
    ↳ HASKELL
      ↳ BR
        ↳ HASKELL
          ↳ COR
            ↳ HASKELL
              ↳ Narrow
                ↳ AND
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                    ↳ DependencyGraphProof
                      ↳ AND
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
QDP
                          ↳ UsableRulesProof
                        ↳ QDP
                        ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_insertBy01(Float(Neg(Zero), Pos(Succ(ww40100))), Float(Neg(Zero), Neg(Succ(Zero))), ww41) → new_insertBy7(ww41)
new_insertBy7(:(ww410, ww411)) → new_insertBy01(ww410, Float(Neg(Zero), Neg(Succ(Zero))), ww411)
new_insertBy01(Float(Pos(Succ(ww40000)), Pos(Succ(ww40100))), Float(Neg(Zero), Neg(Succ(Zero))), ww41) → new_insertBy7(ww41)
new_insertBy01(Float(Neg(Succ(ww40000)), Pos(Succ(ww40100))), Float(Neg(Zero), Neg(Succ(Zero))), :(ww410, ww411)) → new_insertBy01(ww410, Float(Neg(Zero), Neg(Succ(Zero))), ww411)
new_insertBy01(Float(Pos(Zero), Pos(Succ(ww40100))), Float(Neg(Zero), Neg(Succ(Zero))), ww41) → new_insertBy7(ww41)

The TRS R consists of the following rules:

new_primPlusNat1(Zero, ww40000) → Succ(ww40000)
new_primPlusNat0(Zero, Zero) → Zero
new_primMulNat1(Zero, ww40000) → Zero
new_primPlusNat1(Succ(ww550), ww40000) → Succ(Succ(new_primPlusNat0(ww550, ww40000)))
new_primPlusNat0(Succ(ww5500), Zero) → Succ(ww5500)
new_primPlusNat0(Zero, Succ(ww400000)) → Succ(ww400000)
new_primPlusNat0(Succ(ww5500), Succ(ww400000)) → Succ(Succ(new_primPlusNat0(ww5500, ww400000)))
new_primMulNat1(Succ(ww30000), ww40000) → new_primPlusNat1(new_primMulNat1(ww30000, ww40000), ww40000)

The set Q consists of the following terms:

new_primPlusNat0(Succ(x0), Succ(x1))
new_primPlusNat0(Zero, Zero)
new_primPlusNat0(Zero, Succ(x0))
new_primPlusNat0(Succ(x0), Zero)
new_primPlusNat1(Succ(x0), x1)
new_primMulNat1(Zero, x0)
new_primPlusNat1(Zero, x0)
new_primMulNat1(Succ(x0), x1)

We have to consider all minimal (P,Q,R)-chains.
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [15] we can delete all non-usable rules [17] from R.

↳ HASKELL
  ↳ CR
    ↳ HASKELL
      ↳ BR
        ↳ HASKELL
          ↳ COR
            ↳ HASKELL
              ↳ Narrow
                ↳ AND
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                    ↳ DependencyGraphProof
                      ↳ AND
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                          ↳ UsableRulesProof
QDP
                              ↳ QReductionProof
                        ↳ QDP
                        ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_insertBy01(Float(Neg(Zero), Pos(Succ(ww40100))), Float(Neg(Zero), Neg(Succ(Zero))), ww41) → new_insertBy7(ww41)
new_insertBy7(:(ww410, ww411)) → new_insertBy01(ww410, Float(Neg(Zero), Neg(Succ(Zero))), ww411)
new_insertBy01(Float(Pos(Succ(ww40000)), Pos(Succ(ww40100))), Float(Neg(Zero), Neg(Succ(Zero))), ww41) → new_insertBy7(ww41)
new_insertBy01(Float(Neg(Succ(ww40000)), Pos(Succ(ww40100))), Float(Neg(Zero), Neg(Succ(Zero))), :(ww410, ww411)) → new_insertBy01(ww410, Float(Neg(Zero), Neg(Succ(Zero))), ww411)
new_insertBy01(Float(Pos(Zero), Pos(Succ(ww40100))), Float(Neg(Zero), Neg(Succ(Zero))), ww41) → new_insertBy7(ww41)

R is empty.
The set Q consists of the following terms:

new_primPlusNat0(Succ(x0), Succ(x1))
new_primPlusNat0(Zero, Zero)
new_primPlusNat0(Zero, Succ(x0))
new_primPlusNat0(Succ(x0), Zero)
new_primPlusNat1(Succ(x0), x1)
new_primMulNat1(Zero, x0)
new_primPlusNat1(Zero, x0)
new_primMulNat1(Succ(x0), x1)

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.

new_primPlusNat0(Succ(x0), Succ(x1))
new_primPlusNat0(Zero, Zero)
new_primPlusNat0(Zero, Succ(x0))
new_primPlusNat0(Succ(x0), Zero)
new_primPlusNat1(Succ(x0), x1)
new_primMulNat1(Zero, x0)
new_primPlusNat1(Zero, x0)
new_primMulNat1(Succ(x0), x1)



↳ HASKELL
  ↳ CR
    ↳ HASKELL
      ↳ BR
        ↳ HASKELL
          ↳ COR
            ↳ HASKELL
              ↳ Narrow
                ↳ AND
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                    ↳ DependencyGraphProof
                      ↳ AND
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                          ↳ UsableRulesProof
                            ↳ QDP
                              ↳ QReductionProof
QDP
                                  ↳ QDPSizeChangeProof
                        ↳ QDP
                        ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_insertBy7(:(ww410, ww411)) → new_insertBy01(ww410, Float(Neg(Zero), Neg(Succ(Zero))), ww411)
new_insertBy01(Float(Neg(Zero), Pos(Succ(ww40100))), Float(Neg(Zero), Neg(Succ(Zero))), ww41) → new_insertBy7(ww41)
new_insertBy01(Float(Pos(Succ(ww40000)), Pos(Succ(ww40100))), Float(Neg(Zero), Neg(Succ(Zero))), ww41) → new_insertBy7(ww41)
new_insertBy01(Float(Neg(Succ(ww40000)), Pos(Succ(ww40100))), Float(Neg(Zero), Neg(Succ(Zero))), :(ww410, ww411)) → new_insertBy01(ww410, Float(Neg(Zero), Neg(Succ(Zero))), ww411)
new_insertBy01(Float(Pos(Zero), Pos(Succ(ww40100))), Float(Neg(Zero), Neg(Succ(Zero))), ww41) → new_insertBy7(ww41)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ CR
    ↳ HASKELL
      ↳ BR
        ↳ HASKELL
          ↳ COR
            ↳ HASKELL
              ↳ Narrow
                ↳ AND
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                    ↳ DependencyGraphProof
                      ↳ AND
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
QDP
                          ↳ UsableRulesProof
                        ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_insertBy029(ww40100, ww41, Succ(ww2170)) → new_insertBy058(Float(Neg(Zero), Neg(Succ(ww40100))), ww41)
new_insertBy012(ww40000, ww40100, ww41, Succ(ww1020)) → new_insertBy058(Float(Pos(Succ(ww40000)), Neg(Succ(ww40100))), ww41)
new_insertBy01(Float(Neg(Succ(ww40000)), Neg(Succ(ww40100))), Float(Pos(Zero), Pos(Succ(Succ(Zero)))), ww41) → new_insertBy025(ww40000, ww40100, ww41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(ww40100)), Succ(ww40100)))
new_insertBy01(Float(Pos(Zero), Neg(Succ(ww40100))), Float(Pos(Zero), Pos(Succ(Succ(Zero)))), ww41) → new_insertBy016(ww40100, ww41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(ww40100)), Succ(ww40100)))
new_insertBy025(ww40000, ww40100, ww41, Succ(ww1930)) → new_insertBy058(Float(Neg(Succ(ww40000)), Neg(Succ(ww40100))), ww41)
new_insertBy016(ww40100, ww41, Succ(ww1260)) → new_insertBy058(Float(Pos(Zero), Neg(Succ(ww40100))), ww41)
new_insertBy01(Float(Pos(Succ(ww40000)), Neg(Succ(ww40100))), Float(Pos(Zero), Pos(Succ(Succ(Zero)))), ww41) → new_insertBy012(ww40000, ww40100, ww41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(ww40100)), Succ(ww40100)))
new_insertBy01(Float(Neg(Zero), Neg(Succ(ww40100))), Float(Pos(Zero), Pos(Succ(Succ(Zero)))), ww41) → new_insertBy029(ww40100, ww41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(ww40100)), Succ(ww40100)))
new_insertBy058(ww413, :(ww4140, ww4141)) → new_insertBy01(ww4140, Float(Pos(Zero), Pos(Succ(Succ(Zero)))), ww4141)

The TRS R consists of the following rules:

new_primPlusNat1(Zero, ww40000) → Succ(ww40000)
new_primPlusNat0(Zero, Zero) → Zero
new_primMulNat1(Zero, ww40000) → Zero
new_primPlusNat1(Succ(ww550), ww40000) → Succ(Succ(new_primPlusNat0(ww550, ww40000)))
new_primPlusNat0(Succ(ww5500), Zero) → Succ(ww5500)
new_primPlusNat0(Zero, Succ(ww400000)) → Succ(ww400000)
new_primPlusNat0(Succ(ww5500), Succ(ww400000)) → Succ(Succ(new_primPlusNat0(ww5500, ww400000)))
new_primMulNat1(Succ(ww30000), ww40000) → new_primPlusNat1(new_primMulNat1(ww30000, ww40000), ww40000)

The set Q consists of the following terms:

new_primPlusNat0(Succ(x0), Succ(x1))
new_primPlusNat0(Zero, Zero)
new_primPlusNat0(Zero, Succ(x0))
new_primPlusNat0(Succ(x0), Zero)
new_primPlusNat1(Succ(x0), x1)
new_primMulNat1(Zero, x0)
new_primPlusNat1(Zero, x0)
new_primMulNat1(Succ(x0), x1)

We have to consider all minimal (P,Q,R)-chains.
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [15] we can delete all non-usable rules [17] from R.

↳ HASKELL
  ↳ CR
    ↳ HASKELL
      ↳ BR
        ↳ HASKELL
          ↳ COR
            ↳ HASKELL
              ↳ Narrow
                ↳ AND
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                    ↳ DependencyGraphProof
                      ↳ AND
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                          ↳ UsableRulesProof
QDP
                              ↳ QReductionProof
                        ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_insertBy029(ww40100, ww41, Succ(ww2170)) → new_insertBy058(Float(Neg(Zero), Neg(Succ(ww40100))), ww41)
new_insertBy012(ww40000, ww40100, ww41, Succ(ww1020)) → new_insertBy058(Float(Pos(Succ(ww40000)), Neg(Succ(ww40100))), ww41)
new_insertBy01(Float(Neg(Succ(ww40000)), Neg(Succ(ww40100))), Float(Pos(Zero), Pos(Succ(Succ(Zero)))), ww41) → new_insertBy025(ww40000, ww40100, ww41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(ww40100)), Succ(ww40100)))
new_insertBy01(Float(Pos(Zero), Neg(Succ(ww40100))), Float(Pos(Zero), Pos(Succ(Succ(Zero)))), ww41) → new_insertBy016(ww40100, ww41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(ww40100)), Succ(ww40100)))
new_insertBy025(ww40000, ww40100, ww41, Succ(ww1930)) → new_insertBy058(Float(Neg(Succ(ww40000)), Neg(Succ(ww40100))), ww41)
new_insertBy016(ww40100, ww41, Succ(ww1260)) → new_insertBy058(Float(Pos(Zero), Neg(Succ(ww40100))), ww41)
new_insertBy01(Float(Pos(Succ(ww40000)), Neg(Succ(ww40100))), Float(Pos(Zero), Pos(Succ(Succ(Zero)))), ww41) → new_insertBy012(ww40000, ww40100, ww41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(ww40100)), Succ(ww40100)))
new_insertBy01(Float(Neg(Zero), Neg(Succ(ww40100))), Float(Pos(Zero), Pos(Succ(Succ(Zero)))), ww41) → new_insertBy029(ww40100, ww41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(ww40100)), Succ(ww40100)))
new_insertBy058(ww413, :(ww4140, ww4141)) → new_insertBy01(ww4140, Float(Pos(Zero), Pos(Succ(Succ(Zero)))), ww4141)

The TRS R consists of the following rules:

new_primPlusNat0(Zero, Succ(ww400000)) → Succ(ww400000)
new_primPlusNat0(Succ(ww5500), Succ(ww400000)) → Succ(Succ(new_primPlusNat0(ww5500, ww400000)))
new_primPlusNat0(Zero, Zero) → Zero
new_primPlusNat0(Succ(ww5500), Zero) → Succ(ww5500)

The set Q consists of the following terms:

new_primPlusNat0(Succ(x0), Succ(x1))
new_primPlusNat0(Zero, Zero)
new_primPlusNat0(Zero, Succ(x0))
new_primPlusNat0(Succ(x0), Zero)
new_primPlusNat1(Succ(x0), x1)
new_primMulNat1(Zero, x0)
new_primPlusNat1(Zero, x0)
new_primMulNat1(Succ(x0), x1)

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.

new_primPlusNat1(Succ(x0), x1)
new_primMulNat1(Zero, x0)
new_primPlusNat1(Zero, x0)
new_primMulNat1(Succ(x0), x1)



↳ HASKELL
  ↳ CR
    ↳ HASKELL
      ↳ BR
        ↳ HASKELL
          ↳ COR
            ↳ HASKELL
              ↳ Narrow
                ↳ AND
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                    ↳ DependencyGraphProof
                      ↳ AND
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                          ↳ UsableRulesProof
                            ↳ QDP
                              ↳ QReductionProof
QDP
                                  ↳ QDPSizeChangeProof
                        ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_insertBy012(ww40000, ww40100, ww41, Succ(ww1020)) → new_insertBy058(Float(Pos(Succ(ww40000)), Neg(Succ(ww40100))), ww41)
new_insertBy029(ww40100, ww41, Succ(ww2170)) → new_insertBy058(Float(Neg(Zero), Neg(Succ(ww40100))), ww41)
new_insertBy01(Float(Neg(Succ(ww40000)), Neg(Succ(ww40100))), Float(Pos(Zero), Pos(Succ(Succ(Zero)))), ww41) → new_insertBy025(ww40000, ww40100, ww41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(ww40100)), Succ(ww40100)))
new_insertBy01(Float(Pos(Zero), Neg(Succ(ww40100))), Float(Pos(Zero), Pos(Succ(Succ(Zero)))), ww41) → new_insertBy016(ww40100, ww41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(ww40100)), Succ(ww40100)))
new_insertBy025(ww40000, ww40100, ww41, Succ(ww1930)) → new_insertBy058(Float(Neg(Succ(ww40000)), Neg(Succ(ww40100))), ww41)
new_insertBy01(Float(Pos(Succ(ww40000)), Neg(Succ(ww40100))), Float(Pos(Zero), Pos(Succ(Succ(Zero)))), ww41) → new_insertBy012(ww40000, ww40100, ww41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(ww40100)), Succ(ww40100)))
new_insertBy016(ww40100, ww41, Succ(ww1260)) → new_insertBy058(Float(Pos(Zero), Neg(Succ(ww40100))), ww41)
new_insertBy01(Float(Neg(Zero), Neg(Succ(ww40100))), Float(Pos(Zero), Pos(Succ(Succ(Zero)))), ww41) → new_insertBy029(ww40100, ww41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(ww40100)), Succ(ww40100)))
new_insertBy058(ww413, :(ww4140, ww4141)) → new_insertBy01(ww4140, Float(Pos(Zero), Pos(Succ(Succ(Zero)))), ww4141)

The TRS R consists of the following rules:

new_primPlusNat0(Zero, Succ(ww400000)) → Succ(ww400000)
new_primPlusNat0(Succ(ww5500), Succ(ww400000)) → Succ(Succ(new_primPlusNat0(ww5500, ww400000)))
new_primPlusNat0(Zero, Zero) → Zero
new_primPlusNat0(Succ(ww5500), Zero) → Succ(ww5500)

The set Q consists of the following terms:

new_primPlusNat0(Succ(x0), Succ(x1))
new_primPlusNat0(Zero, Zero)
new_primPlusNat0(Zero, Succ(x0))
new_primPlusNat0(Succ(x0), Zero)

We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ CR
    ↳ HASKELL
      ↳ BR
        ↳ HASKELL
          ↳ COR
            ↳ HASKELL
              ↳ Narrow
                ↳ AND
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                    ↳ DependencyGraphProof
                      ↳ AND
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
                        ↳ QDP
QDP
                          ↳ QDPSizeChangeProof

Q DP problem:
The TRS P consists of the following rules:

new_insertBy01(Float(Pos(Zero), Neg(Succ(ww40100))), Float(Pos(Succ(ww3000)), Pos(Succ(Succ(Zero)))), ww41) → new_insertBy08(ww40100, ww3000, ww41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(ww40100)), Succ(ww40100)))
new_insertBy0(ww19, Neg(Succ(ww2000)), ww21, Pos(Succ(ww2200)), ww23, Zero) → new_insertBy03(ww19, ww2000, ww21, ww2200, ww23, new_primPlusNat0(new_primMulNat1(ww2200, ww2000), Succ(ww2000)))
new_insertBy0(ww19, Neg(Zero), ww21, Neg(Succ(ww2200)), ww23, Succ(ww560)) → new_insertBy1(ww21, Succ(ww2200), ww23)
new_insertBy0(ww19, Neg(Succ(ww2000)), ww21, Neg(Zero), ww23, Succ(ww560)) → new_insertBy1(ww21, Zero, ww23)
new_insertBy02(ww19, ww2000, ww21, ww2200, ww23, Succ(ww5600), Succ(Zero)) → new_insertBy088(ww19, ww2000, ww21, ww2200, ww23)
new_insertBy0(ww19, Pos(Succ(ww2000)), ww21, Pos(Zero), ww23, Succ(ww560)) → new_insertBy(ww21, Zero, ww23)
new_insertBy086(ww19, ww200, ww21, ww220, :(ww230, ww231)) → new_insertBy01(ww230, Float(Pos(Succ(ww21)), Neg(ww220)), ww231)
new_insertBy01(Float(Pos(Zero), Neg(Succ(ww40100))), Float(Pos(Succ(ww3000)), Pos(Succ(Succ(Succ(ww310000))))), ww41) → new_insertBy07(ww40100, ww3000, ww310000, ww41, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat1(ww310000, ww40100), Succ(ww40100)), Succ(ww40100)), Succ(ww40100)))
new_insertBy019(ww25, Pos(Succ(ww2600)), ww27, Neg(Succ(ww2800)), ww29, Succ(ww1400)) → new_insertBy060(ww25, ww2600, ww27, ww2800, ww29, new_primPlusNat0(new_primMulNat1(ww2800, ww2600), Succ(ww2600)), ww1400)
new_insertBy05(ww19, ww2000, ww21, ww2200, ww23, Succ(ww5600), Zero) → new_insertBy06(ww19, ww2000, ww21, ww2200, ww23)
new_insertBy085(ww19, ww200, ww21, ww220, :(ww230, ww231)) → new_insertBy01(ww230, Float(Pos(Succ(ww21)), Pos(ww220)), ww231)
new_insertBy06(ww19, ww2000, ww21, ww2200, ww23) → new_insertBy(ww21, Succ(ww2200), ww23)
new_insertBy010(ww40100, ww3000, ww41, Succ(ww720)) → new_insertBy1(ww3000, Succ(Succ(Zero)), ww41)
new_insertBy019(ww25, Neg(Succ(ww2600)), ww27, Pos(Succ(ww2800)), ww29, Zero) → new_insertBy061(ww25, ww2600, ww27, ww2800, ww29, new_primPlusNat0(new_primMulNat1(ww2800, ww2600), Succ(ww2600)))
new_insertBy087(ww19, ww2000, ww21, ww2200, ww23, Succ(ww5600), Succ(ww9000)) → new_insertBy087(ww19, ww2000, ww21, ww2200, ww23, ww5600, ww9000)
new_insertBy0(ww19, Neg(Zero), ww21, Neg(Zero), ww23, Succ(ww560)) → new_insertBy1(ww21, Zero, ww23)
new_insertBy08(ww40100, ww3000, ww41, Succ(ww660)) → new_insertBy(ww3000, Succ(Succ(Zero)), ww41)
new_insertBy0(ww19, Pos(Zero), ww21, Pos(Succ(ww2200)), ww23, Succ(ww560)) → new_insertBy(ww21, Succ(ww2200), ww23)
new_insertBy022(ww40100, ww3000, ww310000, ww41, Succ(ww1590)) → new_insertBy1(ww3000, Succ(Succ(Succ(ww310000))), ww41)
new_insertBy0(ww19, Neg(Succ(ww2000)), ww21, Neg(Succ(ww2200)), ww23, Succ(ww560)) → new_insertBy02(ww19, ww2000, ww21, ww2200, ww23, ww560, new_primPlusNat0(new_primMulNat1(ww2200, ww2000), Succ(ww2000)))
new_insertBy01(Float(Neg(Zero), Pos(Succ(ww40100))), Float(Pos(Succ(ww3000)), Neg(Succ(Succ(Zero)))), ww41) → new_insertBy023(ww40100, ww3000, ww41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(ww40100)), Succ(ww40100)))
new_insertBy062(ww25, ww2600, ww27, ww2800, ww29, Succ(ww1750)) → new_insertBy1(ww27, Succ(ww2800), ww29)
new_insertBy01(Float(Neg(Zero), Pos(Succ(ww40100))), Float(Pos(Succ(ww3000)), Neg(Succ(Succ(Succ(ww310000))))), ww41) → new_insertBy022(ww40100, ww3000, ww310000, ww41, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat1(ww310000, ww40100), Succ(ww40100)), Succ(ww40100)), Succ(ww40100)))
new_insertBy023(ww40100, ww3000, ww41, Succ(ww1630)) → new_insertBy1(ww3000, Succ(Succ(Zero)), ww41)
new_insertBy066(ww25, ww2600, ww27, ww2800, ww29) → new_insertBy1(ww27, Succ(ww2800), ww29)
new_insertBy065(ww25, ww2600, ww27, ww2800, ww29, Succ(ww18100), Succ(ww14000)) → new_insertBy065(ww25, ww2600, ww27, ww2800, ww29, ww18100, ww14000)
new_insertBy059(ww25, ww2600, ww27, ww2800, ww29, Succ(Succ(ww17900)), Zero) → new_insertBy064(ww25, ww2600, ww27, ww2800, ww29)
new_insertBy00(ww19, ww2000, ww21, ww2200, ww23, Succ(ww5600), Succ(Zero)) → new_insertBy06(ww19, ww2000, ww21, ww2200, ww23)
new_insertBy00(ww19, ww2000, ww21, ww2200, ww23, ww560, Zero) → new_insertBy(ww21, Succ(ww2200), ww23)
new_insertBy0(ww19, Pos(Zero), ww21, Pos(Zero), ww23, Succ(ww560)) → new_insertBy(ww21, Zero, ww23)
new_insertBy019(ww25, Neg(Succ(ww2600)), ww27, Pos(Succ(ww2800)), ww29, Succ(ww1400)) → new_insertBy059(ww25, ww2600, ww27, ww2800, ww29, new_primPlusNat0(new_primMulNat1(ww2800, ww2600), Succ(ww2600)), ww1400)
new_insertBy07(ww40100, ww3000, ww310000, ww41, Succ(ww620)) → new_insertBy(ww3000, Succ(Succ(Succ(ww310000))), ww41)
new_insertBy02(ww19, ww2000, ww21, ww2200, ww23, ww560, Zero) → new_insertBy1(ww21, Succ(ww2200), ww23)
new_insertBy01(Float(Pos(Zero), Pos(Succ(ww40100))), Float(Pos(Succ(ww3000)), Neg(Succ(Succ(Succ(ww310000))))), ww41) → new_insertBy09(ww40100, ww3000, ww310000, ww41, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat1(ww310000, ww40100), Succ(ww40100)), Succ(ww40100)), Succ(ww40100)))
new_insertBy088(ww19, ww2000, ww21, ww2200, ww23) → new_insertBy1(ww21, Succ(ww2200), ww23)
new_insertBy00(ww19, ww2000, ww21, ww2200, ww23, Succ(ww5600), Succ(Succ(ww8800))) → new_insertBy05(ww19, ww2000, ww21, ww2200, ww23, ww5600, ww8800)
new_insertBy087(ww19, ww2000, ww21, ww2200, ww23, Succ(ww5600), Zero) → new_insertBy088(ww19, ww2000, ww21, ww2200, ww23)
new_insertBy01(Float(Pos(Zero), Pos(Succ(ww40100))), Float(Pos(Succ(ww3000)), Neg(Succ(Zero))), ww41) → new_insertBy1(ww3000, Succ(Zero), ww41)
new_insertBy0(ww19, Pos(ww200), ww21, Neg(ww220), :(ww230, ww231), Succ(ww560)) → new_insertBy01(ww230, Float(Pos(Succ(ww21)), Neg(ww220)), ww231)
new_insertBy01(Float(Neg(Zero), Pos(Succ(ww40100))), Float(Pos(Succ(ww3000)), Neg(Succ(Zero))), ww41) → new_insertBy1(ww3000, Succ(Zero), ww41)
new_insertBy03(ww19, ww2000, ww21, ww2200, ww23, Succ(ww820)) → new_insertBy085(ww19, Succ(ww2000), ww21, Succ(ww2200), ww23)
new_insertBy01(Float(Pos(Zero), Neg(Succ(ww40100))), Float(Pos(Succ(ww3000)), Pos(Succ(Zero))), ww41) → new_insertBy(ww3000, Succ(Zero), ww41)
new_insertBy04(ww19, ww2000, ww21, ww2200, ww23, Succ(ww840)) → new_insertBy086(ww19, Succ(ww2000), ww21, Succ(ww2200), ww23)
new_insertBy063(ww25, ww2600, ww27, ww2800, ww29, Succ(ww17900), Zero) → new_insertBy064(ww25, ww2600, ww27, ww2800, ww29)
new_insertBy063(ww25, ww2600, ww27, ww2800, ww29, Succ(ww17900), Succ(ww14000)) → new_insertBy063(ww25, ww2600, ww27, ww2800, ww29, ww17900, ww14000)
new_insertBy0(ww19, Pos(Succ(ww2000)), ww21, Pos(Succ(ww2200)), ww23, Succ(ww560)) → new_insertBy00(ww19, ww2000, ww21, ww2200, ww23, ww560, new_primPlusNat0(new_primMulNat1(ww2200, ww2000), Succ(ww2000)))
new_insertBy061(ww25, ww2600, ww27, ww2800, ww29, Succ(ww1730)) → new_insertBy(ww27, Succ(ww2800), ww29)
new_insertBy01(Float(Neg(Zero), Neg(Succ(ww40100))), Float(Pos(Succ(ww3000)), Pos(Succ(Succ(Succ(ww310000))))), ww41) → new_insertBy020(ww40100, ww3000, ww310000, ww41, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat1(ww310000, ww40100), Succ(ww40100)), Succ(ww40100)), Succ(ww40100)))
new_insertBy01(Float(Pos(Zero), Pos(Succ(ww40100))), Float(Pos(Succ(ww3000)), Neg(Succ(Succ(Zero)))), ww41) → new_insertBy010(ww40100, ww3000, ww41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(ww40100)), Succ(ww40100)))
new_insertBy019(ww25, Pos(Succ(ww2600)), ww27, Neg(Succ(ww2800)), ww29, Zero) → new_insertBy062(ww25, ww2600, ww27, ww2800, ww29, new_primPlusNat0(new_primMulNat1(ww2800, ww2600), Succ(ww2600)))
new_insertBy01(Float(Neg(Zero), Neg(Succ(ww40100))), Float(Pos(Succ(ww3000)), Pos(Succ(Zero))), ww41) → new_insertBy(ww3000, Succ(Zero), ww41)
new_insertBy0(ww19, Neg(ww200), ww21, Pos(ww220), :(ww230, ww231), Succ(ww560)) → new_insertBy01(ww230, Float(Pos(Succ(ww21)), Pos(ww220)), ww231)
new_insertBy02(ww19, ww2000, ww21, ww2200, ww23, Succ(ww5600), Succ(Succ(ww9000))) → new_insertBy087(ww19, ww2000, ww21, ww2200, ww23, ww5600, ww9000)
new_insertBy065(ww25, ww2600, ww27, ww2800, ww29, Succ(ww18100), Zero) → new_insertBy066(ww25, ww2600, ww27, ww2800, ww29)
new_insertBy1(ww21, ww220, :(ww230, ww231)) → new_insertBy01(ww230, Float(Pos(Succ(ww21)), Neg(ww220)), ww231)
new_insertBy020(ww40100, ww3000, ww310000, ww41, Succ(ww1530)) → new_insertBy(ww3000, Succ(Succ(Succ(ww310000))), ww41)
new_insertBy059(ww25, ww2600, ww27, ww2800, ww29, Succ(Succ(ww17900)), Succ(ww14000)) → new_insertBy063(ww25, ww2600, ww27, ww2800, ww29, ww17900, ww14000)
new_insertBy01(Float(Neg(Zero), Neg(Succ(ww40100))), Float(Pos(Succ(ww3000)), Pos(Succ(Succ(Zero)))), ww41) → new_insertBy021(ww40100, ww3000, ww41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(ww40100)), Succ(ww40100)))
new_insertBy0(ww19, Pos(Succ(ww2000)), ww21, Neg(Succ(ww2200)), ww23, Zero) → new_insertBy04(ww19, ww2000, ww21, ww2200, ww23, new_primPlusNat0(new_primMulNat1(ww2200, ww2000), Succ(ww2000)))
new_insertBy01(Float(Neg(Succ(ww40000)), ww401), Float(Pos(Succ(ww3000)), ww31), ww41) → new_insertBy019(ww40000, ww401, ww3000, ww31, ww41, new_primPlusNat0(new_primMulNat1(ww3000, ww40000), Succ(ww40000)))
new_insertBy09(ww40100, ww3000, ww310000, ww41, Succ(ww680)) → new_insertBy1(ww3000, Succ(Succ(Succ(ww310000))), ww41)
new_insertBy060(ww25, ww2600, ww27, ww2800, ww29, Succ(Succ(ww18100)), Zero) → new_insertBy066(ww25, ww2600, ww27, ww2800, ww29)
new_insertBy060(ww25, ww2600, ww27, ww2800, ww29, Succ(Succ(ww18100)), Succ(ww14000)) → new_insertBy065(ww25, ww2600, ww27, ww2800, ww29, ww18100, ww14000)
new_insertBy05(ww19, ww2000, ww21, ww2200, ww23, Succ(ww5600), Succ(ww8800)) → new_insertBy05(ww19, ww2000, ww21, ww2200, ww23, ww5600, ww8800)
new_insertBy(ww21, ww220, :(ww230, ww231)) → new_insertBy01(ww230, Float(Pos(Succ(ww21)), Pos(ww220)), ww231)
new_insertBy021(ww40100, ww3000, ww41, Succ(ww1570)) → new_insertBy(ww3000, Succ(Succ(Zero)), ww41)
new_insertBy01(Float(Pos(Succ(ww40000)), ww401), Float(Pos(Succ(ww3000)), ww31), ww41) → new_insertBy0(ww40000, ww401, ww3000, ww31, ww41, new_primPlusNat1(new_primMulNat1(ww3000, ww40000), ww40000))
new_insertBy064(ww25, ww2600, ww27, ww2800, ww29) → new_insertBy(ww27, Succ(ww2800), ww29)

The TRS R consists of the following rules:

new_primPlusNat1(Zero, ww40000) → Succ(ww40000)
new_primPlusNat0(Zero, Zero) → Zero
new_primMulNat1(Zero, ww40000) → Zero
new_primPlusNat1(Succ(ww550), ww40000) → Succ(Succ(new_primPlusNat0(ww550, ww40000)))
new_primPlusNat0(Succ(ww5500), Zero) → Succ(ww5500)
new_primPlusNat0(Zero, Succ(ww400000)) → Succ(ww400000)
new_primPlusNat0(Succ(ww5500), Succ(ww400000)) → Succ(Succ(new_primPlusNat0(ww5500, ww400000)))
new_primMulNat1(Succ(ww30000), ww40000) → new_primPlusNat1(new_primMulNat1(ww30000, ww40000), ww40000)

The set Q consists of the following terms:

new_primPlusNat0(Succ(x0), Succ(x1))
new_primPlusNat0(Zero, Zero)
new_primPlusNat0(Zero, Succ(x0))
new_primPlusNat0(Succ(x0), Zero)
new_primPlusNat1(Succ(x0), x1)
new_primMulNat1(Zero, x0)
new_primPlusNat1(Zero, x0)
new_primMulNat1(Succ(x0), x1)

We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs: